--- 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)