# HG changeset patch
# User wenzelm
# Date 953574554 -3600
# Node ID b0d2002f9f046c8bd1718c6034246cae2f206bd2
# Parent  3a45bc1ff175ec57a089d8154dec12e904a1e5f5
proof methods: 'case_tac' / 'induct_tac';

diff -r 3a45bc1ff175 -r b0d2002f9f04 src/HOL/Tools/datatype_package.ML
--- 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 *)