--- a/src/HOL/Groebner_Basis.thy Wed Feb 10 14:12:02 2010 +0100
+++ b/src/HOL/Groebner_Basis.thy Wed Feb 10 14:12:04 2010 +0100
@@ -556,14 +556,14 @@
fun proc3 phi ss ct =
(case term_of ct of
- Const(@{const_name Algebras.less},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
+ Const(@{const_name Orderings.less},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
let
val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
val _ = map is_number [a,b,c]
val T = ctyp_of_term c
val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_less_eq"}
in SOME (mk_meta_eq th) end
- | Const(@{const_name Algebras.less_eq},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
+ | Const(@{const_name Orderings.less_eq},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
let
val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
val _ = map is_number [a,b,c]
@@ -577,14 +577,14 @@
val T = ctyp_of_term c
val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_eq_eq"}
in SOME (mk_meta_eq th) end
- | Const(@{const_name Algebras.less},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
+ | Const(@{const_name Orderings.less},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
let
val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
val _ = map is_number [a,b,c]
val T = ctyp_of_term c
val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "less_divide_eq"}
in SOME (mk_meta_eq th) end
- | Const(@{const_name Algebras.less_eq},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
+ | Const(@{const_name Orderings.less_eq},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
let
val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
val _ = map is_number [a,b,c]