# HG changeset patch
# User nipkow
# Date 952704896 -3600
# Node ID 65f9089f6f711d06d46e8f6d40d19bf2ba982727
# Parent  d30df828a974d9918d97f4ada8fdee998978ce8f
cases_tac

diff -r d30df828a974 -r 65f9089f6f71 NEWS
--- 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