--- a/src/HOL/Decision_Procs/cooper_tac.ML Thu Apr 12 11:34:50 2012 +0200
+++ b/src/HOL/Decision_Procs/cooper_tac.ML Thu Apr 12 18:39:19 2012 +0200
@@ -6,7 +6,6 @@
sig
val trace: bool Unsynchronized.ref
val linz_tac: Proof.context -> bool -> int -> tactic
- val setup: theory -> theory
end
structure Cooper_Tac: COOPER_TAC =
@@ -115,15 +114,4 @@
| _ => (pre_thm, assm_tac i)
in rtac (((mp_step nh) o (spec_step np)) th) i THEN tac end);
-val setup =
- Method.setup @{binding cooper}
- let
- val parse_flag = Args.$$$ "no_quantify" >> K (K false)
- in
- Scan.lift (Scan.optional (Args.$$$ "(" |-- Scan.repeat1 parse_flag --| Args.$$$ ")") [] >>
- curry (Library.foldl op |>) true) >>
- (fn q => fn ctxt => SIMPLE_METHOD' (linz_tac ctxt q))
- end
- "decision procedure for linear integer arithmetic";
-
end