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

Makarius makarius at sketis.net
Fri Sep 9 16:15:51 CEST 2022

*** 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

This refers to Isabelle/a621e9fb295d.


More information about the isabelle-dev mailing list