# HG changeset patch
# User wenzelm
# Date 972423536 -7200
# Node ID df38c61bf54132f7cb417262d1ae9fd90e7d3084
# Parent  bbaad3045e378067307c1067dd5ab4c2c17e2a7e
* 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
human-readable proof documents.  Please do not include goal states
into document output unless you really know what you are doing!

diff -r bbaad3045e37 -r df38c61bf541 NEWS
--- a/NEWS	Tue Oct 24 23:36:17 2000 +0200
+++ b/NEWS	Tue Oct 24 23:38:56 2000 +0200
@@ -15,6 +15,15 @@
 (should now use \isamath{...} and \isatext{...} in custom symbol
 definitions);
 
+* 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
+human-readable proof documents.  Please do not include goal states
+into document output unless you really know what you are doing!
+
+
 
 *** Isar ***