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

author | wenzelm |

Mon, 13 Mar 2000 13:34:09 +0100 | |

changeset 8440 | d66f0f14b1ca |

parent 8439 | 17e62ef34ec8 |

child 8441 | 18d67c88939c |

* HOL: exhaust_tac on datatypes superceded by new case_tac;
* ML: PureThy.add_thms/add_axioms/add_defs now return theorems;
* Isar/Pure: much better support for case-analysis;
* ML: new combinators |>> and |>>>

--- a/NEWS Mon Mar 13 13:30:49 2000 +0100 +++ b/NEWS Mon Mar 13 13:34:09 2000 +0100 @@ -9,6 +9,10 @@ * HOL: the constant for f``x is now "image" rather than "op ``". +* HOL: exhaust_tac on datatypes superceded by new case_tac; + +* ML: PureThy.add_thms/add_axioms/add_defs now return theorems; + *** Isabelle document preparation *** @@ -24,22 +28,28 @@ *** Isar *** -* names of theorems etc. may be natural numbers as well; - -* intro/elim/dest attributes: changed ! / !! flags to ? / ??; - * Pure now provides its own version of intro/elim/dest attributes; useful for building new logics, but beware of confusion with the Provers/classical ones! -* new 'obtain' language element supports generalized existence proofs; +* Pure: new 'obtain' language element supports generalized existence +proofs; -* HOL: removed "case_split" thm binding, should use "cases" proof +* Pure: much better support for case-analysis type proofs: new 'case' +language element refers to local contexts symbolically, as produced by +certain proof methods; internally, case names are attached to theorems +as "tags"; + +* HOL: new proof method 'cases' and improved version of 'induct' now +support named cases; major packages (inductive, datatype, primrec, +recdef) support case names and properly name parameters; + +* HOL: removed 'case_split' thm binding, should use 'cases' proof method anyway; -* tuned syntax of "induct" method; +* names of theorems etc. may be natural numbers as well; -* new "cases" method for propositions, inductive sets and types; +* intro/elim/dest attributes: changed ! / !! flags to ? / ??; *** HOL *** @@ -53,14 +63,21 @@ * HOL/ex: new theory Factorization proving the Fundamental Theorem of Arithmetic, by Thomas M Rasmussen; -* There is a new tactic "cases_tac" for case distinctions; it subsumes the -old "case_tac" and "exhaust_tac" (which should no longer be used). +* 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 quick-and-dirty +portability; + *** General *** * compression of ML heaps images may now be controlled via -c option of isabelle and isatool usedir; +* new ML combinators |>> and |>>> for incremental transformations with +secondary results (e.g. certain theory extensions): + + New in Isabelle99 (October 1999)