[isabelle-dev] AFP dependencies: Refine_Imperative_HOL

[Mathias Fleury]

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 +
      theories
        "Userguides/Sepref_Chapter_Userguides"
          "Userguides/Sepref_Guide_Quickstart"
          "Userguides/Sepref_Guide_Reference"
          "Userguides/Sepref_Guide_General_Util"


Mathias

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>