# HG changeset patch
# User wenzelm
# Date 957914023 -7200
# Node ID b06d183df34d991b2c3c56fde24e2b8744c40e80
# Parent  d6c92979fa514e4dd3680c6f73e583b394e5deab
tuned;

diff -r d6c92979fa51 -r b06d183df34d NEWS
--- a/NEWS	Tue May 09 16:05:45 2000 +0200
+++ b/NEWS	Wed May 10 01:13:43 2000 +0200
@@ -7,10 +7,12 @@
 
 *** Overview of INCOMPATIBILITIES (see below for more details) ***
 
-* HOL: simplification of natural numbers is much changed.  To partly recover
-       the old behaviour (e.g. to prevent n+n rewriting to #2*n) type
-		Delsimprocs Nat_Numeral_Simprocs.cancel_numerals;
-		Delsimprocs [Nat_Numeral_Simprocs.combine_numerals];
+* HOL: simplification of natural numbers is much changed; to partly
+recover the old behaviour (e.g. to prevent n+n rewriting to #2*n)
+issue the following ML commands:
+
+  Delsimprocs Nat_Numeral_Simprocs.cancel_numerals;
+  Delsimprocs [Nat_Numeral_Simprocs.combine_numerals];
 
 * HOL: the constant for f``x is now "image" rather than "op ``";
 
@@ -24,6 +26,11 @@
 * HOL: the recursion equations generated by 'recdef' are now called
 f.simps instead of f.rules;
 
+* HOL: theory Sexp now in HOL/Induct examples (used to be part of main
+HOL, but was unused); should better use HOL's datatype package anyway;
+
+* HOL/Real: "rabs" replaced by overloaded "abs" function;
+
 * ML: PureThy.add_thms/add_axioms/add_defs return theorems as well;
 
 * LaTeX: several improvements of isabelle.sty;
@@ -115,6 +122,8 @@
 basically a generalized version of de-Bruijn representation; very
 useful in avoiding lifting all operations;
 
+* HOL/Real: "rabs" replaced by overloaded "abs" function;
+
 * greatly improved simplification involving numerals of type nat & int, e.g.
    (i + #8 + j) = Suc k simplifies to  #7 + (i + j) = k
    i*j + k + j*#3*i     simplifies to  #4*(i*j) + k
@@ -123,21 +132,27 @@
   and the term/formula #m*u+x ~~ #n*u+y simplifies simplifies to #(m-n)+x ~~ y
     or x ~~ #(n-m)+y, where ~~ is one of = < <= or - (simproc cancel_numerals);
 
-* new version of "case_tac" subsumes both boolean case split and
+* HOL: new version of "case_tac" subsumes both boolean case split and
 "exhaust_tac" on datatypes; INCOMPATIBILITY: exhaust_tac no longer
 exists, may define val exhaust_tac = case_tac for ad-hoc portability;
 
-* simplification no longer dives into case-expressions: only the selector
-expression is simplified, but not the remaining arms. To enable full
-simplification of case-expressions for datatype t, you need to remove
-t.weak_case_cong from the simpset, either permanently
+* HOL: simplification no longer dives into case-expressions: only the
+selector expression is simplified, but not the remaining arms. To
+enable full simplification of case-expressions for datatype t, you
+need to remove t.weak_case_cong from the simpset, either permanently
 (Delcongs[thm"t.weak_case_cong"];) or locally (delcongs [...]).
 
-* the recursion equations generated by 'recdef' for function 'f' are
-now called f.simps instead of f.rules; if all termination conditions
-are proved automatically, these simplification rules are added to the
-simpset, as in primrec; rules may be named individually as well,
-resulting in a separate list of theorems for each equation;
+* HOL/recdef: the recursion equations generated by 'recdef' for
+function 'f' are now called f.simps instead of f.rules; if all
+termination conditions are proved automatically, these simplification
+rules are added to the simpset, as in primrec; rules may be named
+individually as well, resulting in a separate list of theorems for
+each equation;
+
+* HOL: theorems impI, allI, ballI bound as "strip";
+
+* theory Sexp now in HOL/Induct examples (used to be part of main HOL,
+but was unused);
 
 
 *** General ***