| changeset 23266 | 50f0a4f12ed3 |
| parent 23258 | 9062e98fdab1 |
| child 23312 | 6e32a5bfc30f |
--- a/src/HOL/Groebner_Basis.thy Tue Jun 05 20:46:25 2007 +0200 +++ b/src/HOL/Groebner_Basis.thy Tue Jun 05 22:46:53 2007 +0200 @@ -259,7 +259,7 @@ *} "Semiring_normalizer" -subsection {* Gröbner Bases *} +subsection {* Groebner Bases *} locale semiringb = gb_semiring + assumes add_cancel: "add (x::'a) y = add x z \<longleftrightarrow> y = z"