# HG changeset patch
# User wenzelm
# Date 997216906 -7200
# Node ID d15bb7695339d922bd184a6aaafd799cd0ecd51b
# Parent  4546d8d392213ecfceae8793631d8fd4e8943e3b
tuned;

diff -r 4546d8d39221 -r d15bb7695339 NEWS
--- a/NEWS	Tue Aug 07 22:37:30 2001 +0200
+++ b/NEWS	Tue Aug 07 22:41:46 2001 +0200
@@ -2,31 +2,46 @@
 Isabelle NEWS -- history user-relevant changes
 ==============================================
 
+New in Isabelle2001 (?? 2001)
+-----------------------------
+
+*** HOL ***
+
 * HOL: added "The" definite description operator;
 
-* 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: made split_all_tac safe. EXISTING PROOFS MAY FAIL OR LOOP, so in this
+  (rare) case use   delSWrapper "split_all_tac" addSbefore 
+                    ("unsafe_split_all_tac", unsafe_split_all_tac)
+
+* HOL: added safe wrapper "split_conv_tac" to claset.  EXISTING PROOFS
+MAY FAIL;
 
 * 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.
 
-* 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
-  (rare) case use   delSWrapper "split_all_tac" addSbefore 
-                    ("unsafe_split_all_tac", unsafe_split_all_tac)
-
-* HOL/GroupTheory: group theory examples including Sylow's theorem, by Florian
-  Kammueller;
-
-* ZF: the integer library now covers quotients and remainders, with many laws
-relating division to addition, multiplication, etc.;
+* HOL records: fix problem with user translations by making field
+names appear as syntactic conststants;
+
+* HOL/GroupTheory: group theory examples including Sylow's theorem, by
+Florian Kammueller;
+
+
+*** ZF ***
+
+* ZF: the integer library now covers quotients and remainders, with
+many laws relating division to addition, multiplication, etc.;
+
+
+*** General ***
+
+* Classical reasoner: renamed addaltern to addafter, addSaltern to
+addSafter;
+
+* print modes "type_brackets" and "no_type_brackets" control output of
+nested => (types); the default behaviour is "brackets";
+
 
 
 New in Isabelle99-2 (February 2001)