src/HOL/Tools/datatype_package.ML

         val exh_vname = implode (tl (explode (Syntax.string_of_vname ixn)))
       in res_inst_tac [(exh_vname, aterm)] exhaustion i state end
   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 **)
 
 (* case names *)
 

 
 (** package setup **)
 
 (* setup theory *)
 
-val setup = [DatatypesData.init] @ simproc_setup;
+val setup = [DatatypesData.init, Method.add_methods tactic_emulations] @ simproc_setup;
 
 
 (* outer syntax *)
 
 local structure P = OuterParse and K = OuterSyntax.Keyword in