NEWS
changeset 8848 b06d183df34d
parent 8832 bcceda950cd0
child 8887 c0c583ce0b0b
     1.1 --- a/NEWS	Tue May 09 16:05:45 2000 +0200
     1.2 +++ b/NEWS	Wed May 10 01:13:43 2000 +0200
     1.3 @@ -7,10 +7,12 @@
     1.4  
     1.5  *** Overview of INCOMPATIBILITIES (see below for more details) ***
     1.6  
     1.7 -* HOL: simplification of natural numbers is much changed.  To partly recover
     1.8 -       the old behaviour (e.g. to prevent n+n rewriting to #2*n) type
     1.9 -		Delsimprocs Nat_Numeral_Simprocs.cancel_numerals;
    1.10 -		Delsimprocs [Nat_Numeral_Simprocs.combine_numerals];
    1.11 +* HOL: simplification of natural numbers is much changed; to partly
    1.12 +recover the old behaviour (e.g. to prevent n+n rewriting to #2*n)
    1.13 +issue the following ML commands:
    1.14 +
    1.15 +  Delsimprocs Nat_Numeral_Simprocs.cancel_numerals;
    1.16 +  Delsimprocs [Nat_Numeral_Simprocs.combine_numerals];
    1.17  
    1.18  * HOL: the constant for f``x is now "image" rather than "op ``";
    1.19  
    1.20 @@ -24,6 +26,11 @@
    1.21  * HOL: the recursion equations generated by 'recdef' are now called
    1.22  f.simps instead of f.rules;
    1.23  
    1.24 +* HOL: theory Sexp now in HOL/Induct examples (used to be part of main
    1.25 +HOL, but was unused); should better use HOL's datatype package anyway;
    1.26 +
    1.27 +* HOL/Real: "rabs" replaced by overloaded "abs" function;
    1.28 +
    1.29  * ML: PureThy.add_thms/add_axioms/add_defs return theorems as well;
    1.30  
    1.31  * LaTeX: several improvements of isabelle.sty;
    1.32 @@ -115,6 +122,8 @@
    1.33  basically a generalized version of de-Bruijn representation; very
    1.34  useful in avoiding lifting all operations;
    1.35  
    1.36 +* HOL/Real: "rabs" replaced by overloaded "abs" function;
    1.37 +
    1.38  * greatly improved simplification involving numerals of type nat & int, e.g.
    1.39     (i + #8 + j) = Suc k simplifies to  #7 + (i + j) = k
    1.40     i*j + k + j*#3*i     simplifies to  #4*(i*j) + k
    1.41 @@ -123,21 +132,27 @@
    1.42    and the term/formula #m*u+x ~~ #n*u+y simplifies simplifies to #(m-n)+x ~~ y
    1.43      or x ~~ #(n-m)+y, where ~~ is one of = < <= or - (simproc cancel_numerals);
    1.44  
    1.45 -* new version of "case_tac" subsumes both boolean case split and
    1.46 +* HOL: new version of "case_tac" subsumes both boolean case split and
    1.47  "exhaust_tac" on datatypes; INCOMPATIBILITY: exhaust_tac no longer
    1.48  exists, may define val exhaust_tac = case_tac for ad-hoc portability;
    1.49  
    1.50 -* simplification no longer dives into case-expressions: only the selector
    1.51 -expression is simplified, but not the remaining arms. To enable full
    1.52 -simplification of case-expressions for datatype t, you need to remove
    1.53 -t.weak_case_cong from the simpset, either permanently
    1.54 +* HOL: simplification no longer dives into case-expressions: only the
    1.55 +selector expression is simplified, but not the remaining arms. To
    1.56 +enable full simplification of case-expressions for datatype t, you
    1.57 +need to remove t.weak_case_cong from the simpset, either permanently
    1.58  (Delcongs[thm"t.weak_case_cong"];) or locally (delcongs [...]).
    1.59  
    1.60 -* the recursion equations generated by 'recdef' for function 'f' are
    1.61 -now called f.simps instead of f.rules; if all termination conditions
    1.62 -are proved automatically, these simplification rules are added to the
    1.63 -simpset, as in primrec; rules may be named individually as well,
    1.64 -resulting in a separate list of theorems for each equation;
    1.65 +* HOL/recdef: the recursion equations generated by 'recdef' for
    1.66 +function 'f' are now called f.simps instead of f.rules; if all
    1.67 +termination conditions are proved automatically, these simplification
    1.68 +rules are added to the simpset, as in primrec; rules may be named
    1.69 +individually as well, resulting in a separate list of theorems for
    1.70 +each equation;
    1.71 +
    1.72 +* HOL: theorems impI, allI, ballI bound as "strip";
    1.73 +
    1.74 +* theory Sexp now in HOL/Induct examples (used to be part of main HOL,
    1.75 +but was unused);
    1.76  
    1.77  
    1.78  *** General ***