src/HOL/ex/svc_funcs.ML
changeset 19277 f7602e74d948
parent 19233 77ca20b0ed77
child 19336 fb5e19d26d5e
     1.1 --- a/src/HOL/ex/svc_funcs.ML	Thu Mar 16 20:19:25 2006 +0100
     1.2 +++ b/src/HOL/ex/svc_funcs.ML	Fri Mar 17 09:34:23 2006 +0100
     1.3 @@ -112,8 +112,8 @@
     1.4                           b1 orelse b2)
     1.5                       end
     1.6                   else (*might be numeric equality*) (t, is_intnat T)
     1.7 -           | Const("op <", Type ("fun", [T,_]))  => (t, is_intnat T)
     1.8 -           | Const("op <=", Type ("fun", [T,_])) => (t, is_intnat T)
     1.9 +           | Const("Orderings.less", Type ("fun", [T,_]))  => (t, is_intnat T)
    1.10 +           | Const("Orderings.less_eq", Type ("fun", [T,_])) => (t, is_intnat T)
    1.11             | _ => (t, false)
    1.12           end
    1.13     in #1 o tag end;
    1.14 @@ -219,13 +219,13 @@
    1.15                     else fail t
    1.16              end
    1.17          (*inequalities: possible types are nat, int, real*)
    1.18 -      | fm pos (t as Const("op <",  Type ("fun", [T,_])) $ x $ y) =
    1.19 +      | fm pos (t as Const("Orderings.less",  Type ("fun", [T,_])) $ x $ y) =
    1.20              if not pos orelse T = HOLogic.realT then
    1.21                  Buildin("<", [tm x, tm y])
    1.22              else if is_intnat T then
    1.23                  Buildin("<=", [suc (tm x), tm y])
    1.24              else fail t
    1.25 -      | fm pos (t as Const("op <=",  Type ("fun", [T,_])) $ x $ y) =
    1.26 +      | fm pos (t as Const("Orderings.less_eq",  Type ("fun", [T,_])) $ x $ y) =
    1.27              if pos orelse T = HOLogic.realT then
    1.28                  Buildin("<=", [tm x, tm y])
    1.29              else if is_intnat T then