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