[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