
<html xmlns="http://www.w3.org/1999/xhtml">

<head>

<title></title>

</head>

<body>

<div name="messageBodySection">

<div dir="auto">I was just checking something and noticed that Isabelle/CTT seems to hang if you try e.g.<br />

<br />

<span style="white-space:pre">  isabelle jedit -l CTT ex/Synthesis.thy</span><br />

<br />

On the other hand, <br />

<br />

<span style="white-space:pre">  isabelle jedit -l Pure ex/Synthesis.thy</span><br />

<br />

works perfectly.<br />

<br />

Another thing: with schematic_goal, the display of the proof state really needs to include the schematic goal itself, because it’s getting modified. Obviously this can’t be a priority, but if we’re lucky, the relevant code is still there. </div>

</div>

<div name="messageSignatureSection"><br />

<div class="matchFont">

<div dir="auto">Larry</div>

</div>

</div>

</body>

</html>