src/Tools/induction.ML
changeset 58826 2ed2eaabe3df
parent 56506 c1f04411d43f
child 59582 0fbed69ff081
equal deleted inserted replaced
58825:2065f49da190 58826:2ed2eaabe3df
     1 signature INDUCTION =
     1 signature INDUCTION =
     2 sig
     2 sig
     3   val induction_tac: Proof.context -> bool -> (binding option * (term * bool)) option list list ->
     3   val induction_tac: Proof.context -> bool -> (binding option * (term * bool)) option list list ->
     4     (string * typ) list list -> term option list -> thm list option ->
     4     (string * typ) list list -> term option list -> thm list option ->
     5     thm list -> int -> cases_tactic
     5     thm list -> int -> cases_tactic
     6   val setup: theory -> theory
       
     7 end
     6 end
     8 
     7 
     9 structure Induction: INDUCTION =
     8 structure Induction: INDUCTION =
    10 struct
     9 struct
    11 
    10 
    35         (take n cases ~~ take n hnamess)
    34         (take n cases ~~ take n hnamess)
    36     in ((cases',consumes),th) end
    35     in ((cases',consumes),th) end
    37 
    36 
    38 val induction_tac = Induct.gen_induct_tac (K name_hyps)
    37 val induction_tac = Induct.gen_induct_tac (K name_hyps)
    39 
    38 
    40 val setup = Induct.gen_induct_setup @{binding induction} induction_tac
    39 val _ = Theory.setup (Induct.gen_induct_setup @{binding induction} induction_tac)
    41 
    40 
    42 end
    41 end
    43 
    42