<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body text="#000000" bgcolor="#FFFFFF">
<p>Hello all,<br>
</p>
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).<br>
<br>
<br>
To me, a better change than Makarius' diff would be defining
Refine_Imperative_HOL as Sepref_IICF + Tutorial, probably along the
following lines:<br>
<br>
<blockquote><tt>session Sepref_IICF = </tt><tt><br>
</tt><tt> (*what was previously in Refine_Imperative_HOL except
the Userguide *)</tt><tt><br>
</tt><tt><br>
</tt><tt><br>
</tt><tt>session Refine_Imperative_HOL (AFP) = Sepref_IICF +</tt><tt><br>
</tt><tt> theories</tt><tt><br>
</tt><tt> "Userguides/Sepref_Chapter_Userguides"</tt><tt><br>
</tt><tt> "Userguides/Sepref_Guide_Quickstart"</tt><tt><br>
</tt><tt> "Userguides/Sepref_Guide_Reference"</tt><tt><br>
</tt><tt> "Userguides/Sepref_Guide_General_Util"</tt><br>
</blockquote>
<br>
Mathias<br>
<br>
<div class="moz-cite-prefix">On 12.10.17 23:44, Makarius wrote:<br>
</div>
<blockquote type="cite"
cite="mid:d8136a7d-8155-48af-8119-d7efaa0990e3@sketis.net">
<pre wrap="">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
</pre>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<br>
<pre wrap="">_______________________________________________
isabelle-dev mailing list
<a class="moz-txt-link-abbreviated" href="mailto:isabelle-dev@in.tum.de">isabelle-dev@in.tum.de</a>
<a class="moz-txt-link-freetext" href="https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev</a>
</pre>
</blockquote>
<br>
</body>
</html>