src/HOL/ex/Groebner_Examples.thy
changeset 23331 da040caa0596
parent 23273 c6d5ab154c7c
child 23338 3f1a453cb538
     1.1 --- a/src/HOL/ex/Groebner_Examples.thy	Mon Jun 11 18:28:16 2007 +0200
     1.2 +++ b/src/HOL/ex/Groebner_Examples.thy	Mon Jun 11 18:34:12 2007 +0200
     1.3 @@ -46,6 +46,9 @@
     1.4  theorem "x* (x\<twosuperior> - x  - 5) - 3 = (0::int) \<longleftrightarrow> (x = 3 \<or> x = -1)"
     1.5    by algebra
     1.6  
     1.7 +lemma fixes x::"'a::{idom,recpower,number_ring}"
     1.8 +shows "x^2*y = x^2 & x*y^2 = y^2 \<longleftrightarrow>  x=1 & y=1 | x=0 & y=0"
     1.9 +by algebra
    1.10  
    1.11  subsection {* Lemmas for Lagrange's theorem *}
    1.12