# HG changeset patch
# User wenzelm
# Date 876402409 -7200
# Node ID a17f9b8dca9362325510dec31a390d4032a6f774
# Parent  151d49052228c05930c66a719dd3df9221a0e7e5
no longer handles consts "" -- use syntax instead;
pretty printer: changed order of mixfix annotation preference (again!);

diff -r 151d49052228 -r a17f9b8dca93 NEWS
--- a/NEWS	Thu Oct 09 15:04:21 1997 +0200
+++ b/NEWS	Thu Oct 09 15:06:49 1997 +0200
@@ -22,6 +22,11 @@
 * deleted the obsolete tactical STATE, which was declared by
     fun STATE tacfun st = tacfun st st;
 
+* no longer handles consts "" -- use syntax instead;
+
+* pretty printer: changed order of mixfix annotation preference
+(again!);
+
 
 *** Classical Reasoner ***