proof methods: 'case_tac' / 'induct_tac';
authorwenzelm
Mon Mar 20 18:49:14 2000 +0100 (2000-03-20)
changeset 8541b0d2002f9f04
parent 8540 3a45bc1ff175
child 8542 ac37ba498152
proof methods: 'case_tac' / 'induct_tac';
src/HOL/Tools/datatype_package.ML
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Mon Mar 20 18:48:43 2000 +0100
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Mon Mar 20 18:49:14 2000 +0100
     1.3 @@ -201,6 +201,16 @@
     1.4    end;
     1.5  
     1.6  
     1.7 +(** Isar tactic emulations **)
     1.8 +
     1.9 +fun tactic_syntax tac = #2 oo Method.syntax (Args.goal_spec HEADGOAL -- Scan.lift Args.name >>
    1.10 +  (fn (quant, s) => Method.METHOD (fn facts => quant (Method.insert_tac facts THEN' tac s))));
    1.11 +
    1.12 +val tactic_emulations =
    1.13 + [("induct_tac", tactic_syntax induct_tac, "induct_tac emulation (dynamic instantiation!)"),
    1.14 +  ("case_tac", tactic_syntax case_tac, "case_tac emulation (dynamic instantiation!)")];
    1.15 +
    1.16 +
    1.17  
    1.18  (** induct method setup **)
    1.19  
    1.20 @@ -774,7 +784,7 @@
    1.21  
    1.22  (* setup theory *)
    1.23  
    1.24 -val setup = [DatatypesData.init] @ simproc_setup;
    1.25 +val setup = [DatatypesData.init, Method.add_methods tactic_emulations] @ simproc_setup;
    1.26  
    1.27  
    1.28  (* outer syntax *)