--- a/NEWS Wed Nov 08 14:38:04 2000 +0100
+++ b/NEWS Wed Nov 08 17:46:24 2000 +0100
@@ -1,4 +1,3 @@
-
Isabelle NEWS -- history user-relevant changes
==============================================
@@ -24,8 +23,8 @@
* support sub/super scripts (for single symbols only), input syntax is
like this: "A\<^sup>*" or "A\<^sup>\<star>";
-* antiquotation @{goals} for output of *dynamic* goals state; Note
-that presentation of goal states does not conform to actual
+* antiquotation @{goals} and @{subgoals} for output of *dynamic* goals state;
+Note that presentation of goal states does not conform to actual
human-readable proof documents. Please do not include goal states
into document output unless you really know what you are doing!