src/HOL/Tools/int_arith.ML
changeset 35028 108662d50512
parent 34974 18b41bba42b5
child 35092 cfe605c54e50
     1.1 --- a/src/HOL/Tools/int_arith.ML	Fri Feb 05 14:33:31 2010 +0100
     1.2 +++ b/src/HOL/Tools/int_arith.ML	Fri Feb 05 14:33:50 2010 +0100
     1.3 @@ -71,8 +71,8 @@
     1.4  
     1.5  val lhss' =
     1.6    [@{cpat "(?x::?'a::ring_char_0) = (?y::?'a)"},
     1.7 -   @{cpat "(?x::?'a::ordered_idom) < (?y::?'a)"},
     1.8 -   @{cpat "(?x::?'a::ordered_idom) <= (?y::?'a)"}]
     1.9 +   @{cpat "(?x::?'a::linordered_idom) < (?y::?'a)"},
    1.10 +   @{cpat "(?x::?'a::linordered_idom) <= (?y::?'a)"}]
    1.11  
    1.12  val zero_one_idom_simproc =
    1.13    make_simproc {lhss = lhss' , name = "zero_one_idom_simproc",
    1.14 @@ -80,9 +80,9 @@
    1.15  
    1.16  val fast_int_arith_simproc =
    1.17    Simplifier.simproc @{theory} "fast_int_arith"
    1.18 -     ["(m::'a::{ordered_idom,number_ring}) < n",
    1.19 -      "(m::'a::{ordered_idom,number_ring}) <= n",
    1.20 -      "(m::'a::{ordered_idom,number_ring}) = n"] (K Lin_Arith.simproc);
    1.21 +     ["(m::'a::{linordered_idom,number_ring}) < n",
    1.22 +      "(m::'a::{linordered_idom,number_ring}) <= n",
    1.23 +      "(m::'a::{linordered_idom,number_ring}) = n"] (K Lin_Arith.simproc);
    1.24  
    1.25  val global_setup = Simplifier.map_simpset
    1.26    (fn simpset => simpset addsimprocs [fast_int_arith_simproc]);