# HG changeset patch
# User nipkow
# Date 991727464 -7200
# Node ID 879e53d92f51a4b070af82e629567050dca62194
# Parent  45f837f8889d6453b25632854bb6429f8187d529
*** empty log message ***

diff -r 45f837f8889d -r 879e53d92f51 NEWS
--- a/NEWS	Tue Jun 05 09:41:11 2001 +0200
+++ b/NEWS	Tue Jun 05 09:51:04 2001 +0200
@@ -1,13 +1,16 @@
 Isabelle NEWS -- history user-relevant changes
 ==============================================
 
+* print modes "type_brackets" and "no_type_brackets" control output of nested
+=> (types); the default behaviour is "brackets";
+
+* Classical reasoner: renamed addaltern to addafter, addSaltern to addSafter
+
 * HOL: introduced f^n = f o ... o f
   WARNING: due to the limits of Isabelle's type classes, ^ on functions and
   relations has too general a domain, namely ('a * 'b)set and 'a => 'b.
   This means that it may be necessary to attach explicit type constraints.
 
-* Classical reasoner: renamed addaltern to addafter, addSaltern to addSafter
-
 * HOL: added safe wrapper "split_conv_tac" to claset. EXISTING PROOFS MAY FAIL
 
 * HOL: made split_all_tac safe. EXISTING PROOFS MAY FAIL OR LOOP, so in this