src/HOL/Tools/int_arith.ML
changeset 35092 cfe605c54e50
parent 35028 108662d50512
child 35267 8dfd816713c6
     1.1 --- a/src/HOL/Tools/int_arith.ML	Wed Feb 10 14:12:02 2010 +0100
     1.2 +++ b/src/HOL/Tools/int_arith.ML	Wed Feb 10 14:12:04 2010 +0100
     1.3 @@ -55,7 +55,7 @@
     1.4        @{const_name Algebras.times}, @{const_name Algebras.uminus},
     1.5        @{const_name Algebras.minus}, @{const_name Algebras.plus},
     1.6        @{const_name Algebras.zero},
     1.7 -      @{const_name Algebras.less}, @{const_name Algebras.less_eq}] s
     1.8 +      @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
     1.9    | check (a $ b) = check a andalso check b
    1.10    | check _ = false;
    1.11