src/HOL/Decision_Procs/cooper_tac.ML
changeset 47432 e1576d13e933
parent 47142 d64fa2ca54b8
child 51717 9e7d1c139569
     1.1 --- a/src/HOL/Decision_Procs/cooper_tac.ML	Thu Apr 12 11:34:50 2012 +0200
     1.2 +++ b/src/HOL/Decision_Procs/cooper_tac.ML	Thu Apr 12 18:39:19 2012 +0200
     1.3 @@ -6,7 +6,6 @@
     1.4  sig
     1.5    val trace: bool Unsynchronized.ref
     1.6    val linz_tac: Proof.context -> bool -> int -> tactic
     1.7 -  val setup: theory -> theory
     1.8  end
     1.9  
    1.10  structure Cooper_Tac: COOPER_TAC =
    1.11 @@ -115,15 +114,4 @@
    1.12        | _ => (pre_thm, assm_tac i)
    1.13    in rtac (((mp_step nh) o (spec_step np)) th) i THEN tac end);
    1.14  
    1.15 -val setup =
    1.16 -  Method.setup @{binding cooper}
    1.17 -    let
    1.18 -      val parse_flag = Args.$$$ "no_quantify" >> K (K false)
    1.19 -    in
    1.20 -      Scan.lift (Scan.optional (Args.$$$ "(" |-- Scan.repeat1 parse_flag --| Args.$$$ ")") [] >>
    1.21 -        curry (Library.foldl op |>) true) >>
    1.22 -      (fn q => fn ctxt => SIMPLE_METHOD' (linz_tac ctxt q))
    1.23 -    end
    1.24 -    "decision procedure for linear integer arithmetic";
    1.25 -
    1.26  end