# HG changeset patch
# User nipkow
# Date 973701984 -3600
# Node ID ceaab640734b68fdfe3221c96d3c6a53ef81d95b
# Parent  ef006735bee8999d406336a162843cf150089199
subgoals

diff -r ef006735bee8 -r ceaab640734b NEWS
--- 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!