--- a/src/Tools/induction.ML Sat Dec 12 15:37:42 2015 +0100
+++ b/src/Tools/induction.ML Sun Dec 13 21:56:15 2015 +0100
@@ -7,10 +7,9 @@
signature INDUCTION =
sig
- val induction_tac: Proof.context -> bool ->
- (binding option * (term * bool)) option list list ->
+ val induction_tac: bool -> (binding option * (term * bool)) option list list ->
(string * typ) list list -> term option list -> thm list option ->
- thm list -> int -> cases_tactic
+ thm list -> int -> context_tactic
end
structure Induction: INDUCTION =