[isabelle-dev] AFP dependencies: Refine_Imperative_HOL

Mathias Fleury mathias.fleury at ens-rennes.fr
Fri Oct 13 08:25:22 CEST 2017

Hello all,

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
following lines:

    session Sepref_IICF =
       (*what was previously in Refine_Imperative_HOL except the
    Userguide *)

    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.)
> 	Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20171013/6f241e78/attachment-0002.html>

More information about the isabelle-dev mailing list