--- a/NEWS Tue Feb 13 22:04:09 2001 +0100
+++ b/NEWS Tue Feb 13 22:51:08 2001 +0100
@@ -170,9 +170,6 @@
*** General ***
-* print modes "brackets" and "no_brackets" control output of nested =>
-(types) and ==> (props); the default behaviour is "brackets";
-
* system: support Poly/ML 4.0;
* Pure: the Simplifier has been implemented properly as a derived rule
@@ -180,6 +177,9 @@
penalty in practical applications is about 50%, while reliability of
the Isabelle inference kernel has been greatly improved;
+* print modes "brackets" and "no_brackets" control output of nested =>
+(types) and ==> (props); the default behaviour is "brackets";
+
* Provers: fast_tac (and friends) now handle actual object-logic rules
as assumptions as well;