src/HOL/Decision_Procs/Dense_Linear_Order.thy
changeset 38864 4abe644fcea5
parent 38549 d0385f2764d8
child 41849 1a65b780bd56
     1.1 --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Sat Aug 28 20:24:40 2010 +0800
     1.2 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Sat Aug 28 16:14:32 2010 +0200
     1.3 @@ -519,9 +519,9 @@
     1.4    val [lt, le] = map (Morphism.term phi) [@{term "op \<sqsubset>"}, @{term "op \<sqsubseteq>"}]
     1.5    fun h x t =
     1.6     case term_of t of
     1.7 -     Const(@{const_name "op ="}, _)$y$z => if term_of x aconv y then Ferrante_Rackoff_Data.Eq
     1.8 +     Const(@{const_name HOL.eq}, _)$y$z => if term_of x aconv y then Ferrante_Rackoff_Data.Eq
     1.9                              else Ferrante_Rackoff_Data.Nox
    1.10 -   | @{term "Not"}$(Const(@{const_name "op ="}, _)$y$z) => if term_of x aconv y then Ferrante_Rackoff_Data.NEq
    1.11 +   | @{term "Not"}$(Const(@{const_name HOL.eq}, _)$y$z) => if term_of x aconv y then Ferrante_Rackoff_Data.NEq
    1.12                              else Ferrante_Rackoff_Data.Nox
    1.13     | b$y$z => if Term.could_unify (b, lt) then
    1.14                   if term_of x aconv y then Ferrante_Rackoff_Data.Lt
    1.15 @@ -771,7 +771,7 @@
    1.16        in rth end
    1.17      | _ => Thm.reflexive ct)
    1.18  
    1.19 -|  Const(@{const_name "op ="},_)$_$Const(@{const_name Groups.zero},_) =>
    1.20 +|  Const(@{const_name HOL.eq},_)$_$Const(@{const_name Groups.zero},_) =>
    1.21     (case whatis x (Thm.dest_arg1 ct) of
    1.22      ("c*x+t",[c,t]) =>
    1.23         let
    1.24 @@ -835,7 +835,7 @@
    1.25         val rth = Thm.transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
    1.26     in rth end
    1.27  
    1.28 -| Const(@{const_name "op ="},_)$a$b =>
    1.29 +| Const(@{const_name HOL.eq},_)$a$b =>
    1.30     let val (ca,cb) = Thm.dest_binop ct
    1.31         val T = ctyp_of_term ca
    1.32         val th = instantiate' [SOME T] [SOME ca, SOME cb] eq_iff_diff_eq_0
    1.33 @@ -844,7 +844,7 @@
    1.34                (Semiring_Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th
    1.35         val rth = Thm.transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
    1.36     in rth end
    1.37 -| @{term "Not"} $(Const(@{const_name "op ="},_)$a$b) => Conv.arg_conv (field_isolate_conv phi ctxt vs) ct
    1.38 +| @{term "Not"} $(Const(@{const_name HOL.eq},_)$a$b) => Conv.arg_conv (field_isolate_conv phi ctxt vs) ct
    1.39  | _ => Thm.reflexive ct
    1.40  end;
    1.41  
    1.42 @@ -852,9 +852,9 @@
    1.43   let
    1.44    fun h x t =
    1.45     case term_of t of
    1.46 -     Const(@{const_name "op ="}, _)$y$z => if term_of x aconv y then Ferrante_Rackoff_Data.Eq
    1.47 +     Const(@{const_name HOL.eq}, _)$y$z => if term_of x aconv y then Ferrante_Rackoff_Data.Eq
    1.48                              else Ferrante_Rackoff_Data.Nox
    1.49 -   | @{term "Not"}$(Const(@{const_name "op ="}, _)$y$z) => if term_of x aconv y then Ferrante_Rackoff_Data.NEq
    1.50 +   | @{term "Not"}$(Const(@{const_name HOL.eq}, _)$y$z) => if term_of x aconv y then Ferrante_Rackoff_Data.NEq
    1.51                              else Ferrante_Rackoff_Data.Nox
    1.52     | Const(@{const_name Orderings.less},_)$y$z =>
    1.53         if term_of x aconv y then Ferrante_Rackoff_Data.Lt