NEWS
changeset 8412 65f9089f6f71
parent 8392 5bf82327aa36
child 8425 f03c667cf702
     1.1 --- a/NEWS	Fri Mar 10 15:03:05 2000 +0100
     1.2 +++ b/NEWS	Fri Mar 10 17:14:56 2000 +0100
     1.3 @@ -7,6 +7,8 @@
     1.4  
     1.5  *** Overview of INCOMPATIBILITIES (see below for more details) ***
     1.6  
     1.7 +* HOL: "case_tac" is now called "cases_tac" (see below)
     1.8 +
     1.9  * HOL: the constant for f``x is now "image" rather than "op ``".
    1.10  
    1.11  
    1.12 @@ -53,6 +55,10 @@
    1.13  * HOL/ex: new theory Factorization proving the Fundamental Theorem of
    1.14  Arithmetic, by Thomas M Rasmussen;
    1.15  
    1.16 +* There is a new tactic "cases_tac" for case distinctions; it subsumes the
    1.17 +old "case_tac" (no longer available) and "exhaust_tac" (which should no
    1.18 +longer be used).
    1.19 +
    1.20  *** General ***
    1.21  
    1.22  * compression of ML heaps images may now be controlled via -c option