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

[Makarius]

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