src/HOL/Tools/Function/induction_schema.ML
changeset 47432 e1576d13e933
parent 46467 39e412f9ffdf
child 51717 9e7d1c139569
     1.1 --- a/src/HOL/Tools/Function/induction_schema.ML	Thu Apr 12 11:34:50 2012 +0200
     1.2 +++ b/src/HOL/Tools/Function/induction_schema.ML	Thu Apr 12 18:39:19 2012 +0200
     1.3 @@ -9,7 +9,6 @@
     1.4    val mk_ind_tac : (int -> tactic) -> (int -> tactic) -> (int -> tactic)
     1.5                     -> Proof.context -> thm list -> tactic
     1.6    val induction_schema_tac : Proof.context -> thm list -> tactic
     1.7 -  val setup : theory -> theory
     1.8  end
     1.9  
    1.10  
    1.11 @@ -395,8 +394,4 @@
    1.12  fun induction_schema_tac ctxt =
    1.13    mk_ind_tac (K all_tac) (assume_tac APPEND' Goal.assume_rule_tac ctxt) (K all_tac) ctxt;
    1.14  
    1.15 -val setup =
    1.16 -  Method.setup @{binding induction_schema} (Scan.succeed (RAW_METHOD o induction_schema_tac))
    1.17 -    "proves an induction principle"
    1.18 -
    1.19  end