Display of schematic goal instance
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.
- Projects
- None
- Subscribers
- None