*** 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
[email protected]
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
