cases_tac
authornipkow
Fri Mar 10 17:14:56 2000 +0100 (2000-03-10)
changeset 841265f9089f6f71
parent 8411 d30df828a974
child 8413 09db77a084aa
cases_tac
NEWS
     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