--- a/src/HOL/Tools/Function/induction_schema.ML Thu Apr 12 11:34:50 2012 +0200
+++ b/src/HOL/Tools/Function/induction_schema.ML Thu Apr 12 18:39:19 2012 +0200
@@ -9,7 +9,6 @@
val mk_ind_tac : (int -> tactic) -> (int -> tactic) -> (int -> tactic)
-> Proof.context -> thm list -> tactic
val induction_schema_tac : Proof.context -> thm list -> tactic
- val setup : theory -> theory
end
@@ -395,8 +394,4 @@
fun induction_schema_tac ctxt =
mk_ind_tac (K all_tac) (assume_tac APPEND' Goal.assume_rule_tac ctxt) (K all_tac) ctxt;
-val setup =
- Method.setup @{binding induction_schema} (Scan.succeed (RAW_METHOD o induction_schema_tac))
- "proves an induction principle"
-
end