--- a/src/HOL/Groebner_Basis.thy Thu May 06 17:55:12 2010 +0200 +++ b/src/HOL/Groebner_Basis.thy Thu May 06 17:59:19 2010 +0200 @@ -589,8 +589,6 @@ end *} -lemmas comp_arith = semiring_norm (*FIXME*) - subsection {* Groebner Bases *}