Stream: Mirror: Isabelle Development Mailing List

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

Email Gateway (Sep 09 2022 at 14:16):

From: Makarius <makarius@sketis.net>
* General *

• The instantiation of schematic goals is now displayed explicitly as a
  list of variable assignments. This works for proof state output, and at
  the end of a toplevel proof. In rare situations, a proof command or
  proof method may violate the intended goal discipline, by not producing
  an instance of the original goal, but there is only a warning, no hard
  error.

This refers to Isabelle/a621e9fb295d.

Makarius

isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

Email Gateway (Sep 09 2022 at 16:02):

From: Makarius <makarius@sketis.net>
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

isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

Last updated: Apr 24 2024 at 20:16 UTC