NEWS
changeset 9746 64b803edef39
parent 9741 0502f06c2d29
child 9753 f25ac7194f71
--- 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;