Display of schematic goal instance
- 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.
Written by makarius on Sep 9 2022, 4:05 PM.