src/Tools/induction.ML
changeset 61841 4d3527b94f2a
parent 59970 e9f73d87d904
child 61844 007d3b34080f
     1.1 --- a/src/Tools/induction.ML	Sat Dec 12 15:37:42 2015 +0100
     1.2 +++ b/src/Tools/induction.ML	Sun Dec 13 21:56:15 2015 +0100
     1.3 @@ -7,10 +7,9 @@
     1.4  
     1.5  signature INDUCTION =
     1.6  sig
     1.7 -  val induction_tac: Proof.context -> bool ->
     1.8 -    (binding option * (term * bool)) option list list ->
     1.9 +  val induction_tac: bool -> (binding option * (term * bool)) option list list ->
    1.10      (string * typ) list list -> term option list -> thm list option ->
    1.11 -    thm list -> int -> cases_tactic
    1.12 +    thm list -> int -> context_tactic
    1.13  end
    1.14  
    1.15  structure Induction: INDUCTION =