[isabelle-dev] Isabelle/CTT

[Lawrence Paulson]

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

works perfectly.

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.

Larry
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20220901/ac5d884e/attachment.htm>