src/HOL/Groebner_Basis.thy
changeset 35092 cfe605c54e50
parent 35084 e25eedfc15ce
child 35216 7641e8d831d2
     1.1 --- a/src/HOL/Groebner_Basis.thy	Wed Feb 10 14:12:02 2010 +0100
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Wed Feb 10 14:12:04 2010 +0100
     1.3 @@ -556,14 +556,14 @@
     1.4  
     1.5   fun proc3 phi ss ct =
     1.6    (case term_of ct of
     1.7 -    Const(@{const_name Algebras.less},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
     1.8 +    Const(@{const_name Orderings.less},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
     1.9        let
    1.10          val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
    1.11          val _ = map is_number [a,b,c]
    1.12          val T = ctyp_of_term c
    1.13          val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_less_eq"}
    1.14        in SOME (mk_meta_eq th) end
    1.15 -  | Const(@{const_name Algebras.less_eq},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
    1.16 +  | Const(@{const_name Orderings.less_eq},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
    1.17        let
    1.18          val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
    1.19          val _ = map is_number [a,b,c]
    1.20 @@ -577,14 +577,14 @@
    1.21          val T = ctyp_of_term c
    1.22          val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_eq_eq"}
    1.23        in SOME (mk_meta_eq th) end
    1.24 -  | Const(@{const_name Algebras.less},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
    1.25 +  | Const(@{const_name Orderings.less},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
    1.26      let
    1.27        val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
    1.28          val _ = map is_number [a,b,c]
    1.29          val T = ctyp_of_term c
    1.30          val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "less_divide_eq"}
    1.31        in SOME (mk_meta_eq th) end
    1.32 -  | Const(@{const_name Algebras.less_eq},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
    1.33 +  | Const(@{const_name Orderings.less_eq},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
    1.34      let
    1.35        val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
    1.36          val _ = map is_number [a,b,c]