proof methods: 'case_tac' / 'induct_tac';

--- a/src/HOL/Tools/datatype_package.ML	Mon Mar 20 18:48:43 2000 +0100
+++ b/src/HOL/Tools/datatype_package.ML	Mon Mar 20 18:49:14 2000 +0100
@@ -201,6 +201,16 @@
   end;
 
 
+(** Isar tactic emulations **)
+
+fun tactic_syntax tac = #2 oo Method.syntax (Args.goal_spec HEADGOAL -- Scan.lift Args.name >>
+  (fn (quant, s) => Method.METHOD (fn facts => quant (Method.insert_tac facts THEN' tac s))));
+
+val tactic_emulations =
+ [("induct_tac", tactic_syntax induct_tac, "induct_tac emulation (dynamic instantiation!)"),
+  ("case_tac", tactic_syntax case_tac, "case_tac emulation (dynamic instantiation!)")];
+
+
 
 (** induct method setup **)
 
@@ -774,7 +784,7 @@
 
 (* setup theory *)
 
-val setup = [DatatypesData.init] @ simproc_setup;
+val setup = [DatatypesData.init, Method.add_methods tactic_emulations] @ simproc_setup;
 
 
 (* outer syntax *)