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