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

NEWS

changeset 8440 | d66f0f14b1ca |

parent 8425 | f03c667cf702 |

child 8487 | 5f3b0e02ec15 |

1.1 --- a/NEWS Mon Mar 13 13:30:49 2000 +0100 1.2 +++ b/NEWS Mon Mar 13 13:34:09 2000 +0100 1.3 @@ -9,6 +9,10 @@ 1.4 1.5 * HOL: the constant for f``x is now "image" rather than "op ``". 1.6 1.7 +* HOL: exhaust_tac on datatypes superceded by new case_tac; 1.8 + 1.9 +* ML: PureThy.add_thms/add_axioms/add_defs now return theorems; 1.10 + 1.11 1.12 *** Isabelle document preparation *** 1.13 1.14 @@ -24,22 +28,28 @@ 1.15 1.16 *** Isar *** 1.17 1.18 -* names of theorems etc. may be natural numbers as well; 1.19 - 1.20 -* intro/elim/dest attributes: changed ! / !! flags to ? / ??; 1.21 - 1.22 * Pure now provides its own version of intro/elim/dest attributes; 1.23 useful for building new logics, but beware of confusion with the 1.24 Provers/classical ones! 1.25 1.26 -* new 'obtain' language element supports generalized existence proofs; 1.27 +* Pure: new 'obtain' language element supports generalized existence 1.28 +proofs; 1.29 1.30 -* HOL: removed "case_split" thm binding, should use "cases" proof 1.31 +* Pure: much better support for case-analysis type proofs: new 'case' 1.32 +language element refers to local contexts symbolically, as produced by 1.33 +certain proof methods; internally, case names are attached to theorems 1.34 +as "tags"; 1.35 + 1.36 +* HOL: new proof method 'cases' and improved version of 'induct' now 1.37 +support named cases; major packages (inductive, datatype, primrec, 1.38 +recdef) support case names and properly name parameters; 1.39 + 1.40 +* HOL: removed 'case_split' thm binding, should use 'cases' proof 1.41 method anyway; 1.42 1.43 -* tuned syntax of "induct" method; 1.44 +* names of theorems etc. may be natural numbers as well; 1.45 1.46 -* new "cases" method for propositions, inductive sets and types; 1.47 +* intro/elim/dest attributes: changed ! / !! flags to ? / ??; 1.48 1.49 1.50 *** HOL *** 1.51 @@ -53,14 +63,21 @@ 1.52 * HOL/ex: new theory Factorization proving the Fundamental Theorem of 1.53 Arithmetic, by Thomas M Rasmussen; 1.54 1.55 -* There is a new tactic "cases_tac" for case distinctions; it subsumes the 1.56 -old "case_tac" and "exhaust_tac" (which should no longer be used). 1.57 +* new version of "case_tac" subsumes both boolean case split and 1.58 +"exhaust_tac" on datatypes; INCOMPATIBILITY: exhaust_tac no longer 1.59 +exists, may define val exhaust_tac = case_tac for quick-and-dirty 1.60 +portability; 1.61 + 1.62 1.63 *** General *** 1.64 1.65 * compression of ML heaps images may now be controlled via -c option 1.66 of isabelle and isatool usedir; 1.67 1.68 +* new ML combinators |>> and |>>> for incremental transformations with 1.69 +secondary results (e.g. certain theory extensions): 1.70 + 1.71 + 1.72 1.73 1.74 New in Isabelle99 (October 1999)