--- 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;