# HG changeset patch
# User wenzelm
# Date 1662725346 -7200
# Node ID a621e9fb295d5974f3d8470d172a2ed639b1054c
# Parent  7cac5565e79bcae21f6290a15a2a3e3de75b42fc
NEWS;

diff -r 7cac5565e79b -r a621e9fb295d NEWS
--- 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