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]
```