summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Wed, 10 May 2000 01:13:43 +0200 | |

changeset 8848 | b06d183df34d |

parent 8847 | d6c92979fa51 |

child 8849 | f1933a670ae4 |

tuned;

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