--- a/NEWS Fri Mar 10 15:03:05 2000 +0100
+++ b/NEWS Fri Mar 10 17:14:56 2000 +0100
@@ -7,6 +7,8 @@
*** Overview of INCOMPATIBILITIES (see below for more details) ***
+* HOL: "case_tac" is now called "cases_tac" (see below)
+
* HOL: the constant for f``x is now "image" rather than "op ``".
@@ -53,6 +55,10 @@
* HOL/ex: new theory Factorization proving the Fundamental Theorem of
Arithmetic, by Thomas M Rasmussen;
+* There is a new tactic "cases_tac" for case distinctions; it subsumes the
+old "case_tac" (no longer available) and "exhaust_tac" (which should no
+longer be used).
+
*** General ***
* compression of ML heaps images may now be controlled via -c option