src/HOL/Tools/Qelim/cooper.ML
changeset 38864 4abe644fcea5
parent 38808 89ae86205739
child 39159 0dec18004e75
     1.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Sat Aug 28 20:24:40 2010 +0800
     1.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Sat Aug 28 16:14:32 2010 +0200
     1.3 @@ -122,8 +122,8 @@
     1.4  ( case (term_of ct) of
     1.5    Const(@{const_name HOL.conj},_)$_$_ => And (Thm.dest_binop ct)
     1.6  | Const (@{const_name HOL.disj},_)$_$_ => Or (Thm.dest_binop ct)
     1.7 -| Const (@{const_name "op ="},_)$y$_ => if term_of x aconv y then Eq (Thm.dest_arg ct) else Nox
     1.8 -| Const (@{const_name Not},_) $ (Const (@{const_name "op ="},_)$y$_) =>
     1.9 +| Const (@{const_name HOL.eq},_)$y$_ => if term_of x aconv y then Eq (Thm.dest_arg ct) else Nox
    1.10 +| Const (@{const_name Not},_) $ (Const (@{const_name HOL.eq},_)$y$_) =>
    1.11    if term_of x aconv y then NEq (funpow 2 Thm.dest_arg ct) else Nox
    1.12  | Const (@{const_name Orderings.less}, _) $ y$ z =>
    1.13     if term_of x aconv y then Lt (Thm.dest_arg ct)
    1.14 @@ -274,7 +274,7 @@
    1.15    | lin vs (Const (@{const_name Not},T)$t) = Const (@{const_name Not},T)$ (lin vs t)
    1.16    | lin (vs as x::_) (Const(@{const_name Rings.dvd},_)$d$t) =
    1.17      HOLogic.mk_binrel @{const_name Rings.dvd} (numeral1 abs d, lint vs t)
    1.18 -  | lin (vs as x::_) ((b as Const(@{const_name "op ="},_))$s$t) =
    1.19 +  | lin (vs as x::_) ((b as Const(@{const_name HOL.eq},_))$s$t) =
    1.20       (case lint vs (subC$t$s) of
    1.21        (t as a$(m$c$y)$r) =>
    1.22          if x <> y then b$zero$t
    1.23 @@ -345,7 +345,7 @@
    1.24     case (term_of t) of
    1.25      Const(s,_)$(Const(@{const_name Groups.times},_)$c$y)$ _ =>
    1.26      if x aconv y andalso member (op =)
    1.27 -      ["op =", @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
    1.28 +      [@{const_name HOL.eq}, @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
    1.29      then (ins (dest_number c) acc,dacc) else (acc,dacc)
    1.30    | Const(s,_)$_$(Const(@{const_name Groups.times},_)$c$y) =>
    1.31      if x aconv y andalso member (op =)
    1.32 @@ -387,7 +387,7 @@
    1.33    | Const (@{const_name Not},_)$_ => Conv.arg_conv unit_conv t
    1.34    | Const(s,_)$(Const(@{const_name Groups.times},_)$c$y)$ _ =>
    1.35      if x=y andalso member (op =)
    1.36 -      ["op =", @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
    1.37 +      [@{const_name HOL.eq}, @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
    1.38      then cv (l div dest_number c) t else Thm.reflexive t
    1.39    | Const(s,_)$_$(Const(@{const_name Groups.times},_)$c$y) =>
    1.40      if x=y andalso member (op =)