--- a/NEWS Fri Sep 09 14:03:29 2022 +0200
+++ b/NEWS Fri Sep 09 14:09:06 2022 +0200
@@ -21,6 +21,13 @@
- "chapter_definition NAME description TEXT" to provide a description
for presentation purposes
+* 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.
+
* System option "show_states" controls output of toplevel command states
(notably proof states) in batch-builds; in interactive mode this is
always done on demand. The option is relevant for tools that operate on