src/HOL/Tools/int_arith.ML
changeset 31101 26c7bb764a38
parent 31100 6a2e67fe4488
child 31510 e0f2bb4b0021
     1.1 --- a/src/HOL/Tools/int_arith.ML	Mon May 11 15:18:32 2009 +0200
     1.2 +++ b/src/HOL/Tools/int_arith.ML	Mon May 11 15:57:29 2009 +0200
     1.3 @@ -82,7 +82,7 @@
     1.4    Simplifier.simproc @{theory} "fast_int_arith"
     1.5       ["(m::'a::{ordered_idom,number_ring}) < n",
     1.6        "(m::'a::{ordered_idom,number_ring}) <= n",
     1.7 -      "(m::'a::{ordered_idom,number_ring}) = n"] (K Lin_Arith.lin_arith_simproc);
     1.8 +      "(m::'a::{ordered_idom,number_ring}) = n"] (K Lin_Arith.simproc);
     1.9  
    1.10  val global_setup = Simplifier.map_simpset
    1.11    (fn simpset => simpset addsimprocs [fast_int_arith_simproc]);