[isabelle-dev] NEWS: Display of schematic goal instance

Makarius makarius at sketis.net
Fri Sep 9 17:53:14 CEST 2022


On 09/09/2022 17:32, Lawrence Paulson wrote:
> Many thanks for taking care of this. It looks a lot better than what we have long ago. Now let’s just hope somebody uses it. I’m planning to publicise it myself after the next release.

OK. If this is going to be a blog entry about CTT or other "minor 
object-logics", you can just tell readers to use regular Isabelle/HOL within 
Isabelle/jEdit and direct the editor to the example files.  Everything will be 
loaded on the spot: these applications are very small for today's standards.


	Makarius


More information about the isabelle-dev mailing list