# HG changeset patch
# User nipkow
# Date 1181579652 -7200
# Node ID da040caa059654d9cc5a05b1042a3ef05c9b6a3e
# Parent  01c09922ce59affdef2fc80e18a972fdef8344a1
nex example

diff -r 01c09922ce59 -r da040caa0596 src/HOL/ex/Groebner_Examples.thy
--- 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 *}