[isabelle-dev] AFP dependencies: Refine_Imperative_HOL
mathias.fleury at ens-rennes.fr
Fri Oct 13 08:25:22 CEST 2017
as a user of the Refinement Framework, there is a key difference between
the sessions Sepref_IICF and Refine_Imperative_HOL: the former does not
include the tutorial while the latter does. I find it extremely useful
to be able to use Sepref_IICF as parent session and still be able to run
the tutorial (without opening a new Isabelle window that has to load the
full IICF session).
To me, a better change than Makarius' diff would be defining
Refine_Imperative_HOL as Sepref_IICF + Tutorial, probably along the
session Sepref_IICF =
(*what was previously in Refine_Imperative_HOL except the
session Refine_Imperative_HOL (AFP) = Sepref_IICF +
On 12.10.17 23:44, Makarius wrote:
> Here is some further simplification proposed by "isabelle imports -I".
> One could probably also eliminate Sepref_Prereq. The maintainers of
> these AFP entries need to say what is the purpose of that extra complexity.
> (In the months before the Isabelle2017 release, I spent considerable
> time to disentangle Sepref_Prereq, Refine_Imperative_HOL, Sepref_Basic,
> Sepref_IICF -- and only now it becomes clear that there is not much
> behind it.)
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the isabelle-dev