nex example

--- a/src/HOL/ex/Groebner_Examples.thy	Mon Jun 11 18:28:16 2007 +0200
+++ b/src/HOL/ex/Groebner_Examples.thy	Mon Jun 11 18:34:12 2007 +0200
@@ -46,6 +46,9 @@
 theorem "x* (x\<twosuperior> - x  - 5) - 3 = (0::int) \<longleftrightarrow> (x = 3 \<or> x = -1)"
   by algebra
 
+lemma fixes x::"'a::{idom,recpower,number_ring}"
+shows "x^2*y = x^2 & x*y^2 = y^2 \<longleftrightarrow>  x=1 & y=1 | x=0 & y=0"
+by algebra
 
 subsection {* Lemmas for Lagrange's theorem *}