lawrencecpaulson at icloud.com
Thu Sep 1 20:09:18 CEST 2022
I was just checking something and noticed that Isabelle/CTT seems to hang if you try e.g.
isabelle jedit -l CTT ex/Synthesis.thy
On the other hand,
isabelle jedit -l Pure ex/Synthesis.thy
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.
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the isabelle-dev