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)