summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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