# HG changeset patch
# User nipkow
# Date 967645469 -7200
# Node ID 64b803edef396c5897eb080549cb76330f1e2eca
# Parent  07f2487f1abbabd6ceafbca41ff575f75f970475
*** empty log message ***

diff -r 07f2487f1abb -r 64b803edef39 NEWS
--- a/NEWS	Wed Aug 30 15:30:19 2000 +0200
+++ b/NEWS	Wed Aug 30 16:24:29 2000 +0200
@@ -1,4 +1,3 @@
-
 Isabelle NEWS -- history user-relevant changes
 ==============================================
 
@@ -281,6 +280,10 @@
 
 * HOL: theorems impI, allI, ballI bound as "strip";
 
+* new tactic induct_thm_tac: thm -> string -> int -> tactic
+induct_tac th "x1 ... xn" expects th to have a conclusion of the form
+P v1 ... vn and abbreviates res_inst_tac [("v1","x1"),...,("vn","xn")] th;
+
 * new function rulify: thm -> thm for turning outer -->/! into ==>/?;
 behaves like qed_spec_mp;