NEWS
changeset 8425 f03c667cf702
parent 8412 65f9089f6f71
child 8440 d66f0f14b1ca
     1.1 --- a/NEWS	Mon Mar 13 13:11:16 2000 +0100
     1.2 +++ b/NEWS	Mon Mar 13 13:13:46 2000 +0100
     1.3 @@ -7,8 +7,6 @@
     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 @@ -56,8 +54,7 @@
    1.13  Arithmetic, by Thomas M Rasmussen;
    1.14  
    1.15  * There is a new tactic "cases_tac" for case distinctions; it subsumes the
    1.16 -old "case_tac" (no longer available) and "exhaust_tac" (which should no
    1.17 -longer be used).
    1.18 +old "case_tac" and "exhaust_tac" (which should no longer be used).
    1.19  
    1.20  *** General ***
    1.21