src/HOL/Tools/int_arith.ML
changeset 43595 7ae4a23b5be6
parent 42795 66fcc9882784
child 47108 2a1953f0d20d
     1.1 --- a/src/HOL/Tools/int_arith.ML	Wed Jun 29 17:35:46 2011 +0200
     1.2 +++ b/src/HOL/Tools/int_arith.ML	Wed Jun 29 18:12:34 2011 +0200
     1.3 @@ -6,7 +6,6 @@
     1.4  signature INT_ARITH =
     1.5  sig
     1.6    val setup: Context.generic -> Context.generic
     1.7 -  val global_setup: theory -> theory
     1.8  end
     1.9  
    1.10  structure Int_Arith : INT_ARITH =
    1.11 @@ -78,16 +77,6 @@
    1.12    make_simproc {lhss = lhss' , name = "zero_one_idom_simproc",
    1.13    proc = sproc, identifier = []}
    1.14  
    1.15 -val fast_int_arith_simproc =
    1.16 -  Simplifier.simproc_global @{theory} "fast_int_arith"
    1.17 -     ["(m::'a::{linordered_idom,number_ring}) < n",
    1.18 -      "(m::'a::{linordered_idom,number_ring}) <= n",
    1.19 -      "(m::'a::{linordered_idom,number_ring}) = n"] (K Lin_Arith.simproc);
    1.20 -
    1.21 -val global_setup =
    1.22 -  Simplifier.map_simpset_global (fn ss => ss addsimprocs [fast_int_arith_simproc]);
    1.23 -
    1.24 -
    1.25  fun number_of thy T n =
    1.26    if not (Sign.of_sort thy (T, @{sort number}))
    1.27    then raise CTERM ("number_of", [])