src/HOL/ex/Groebner_Examples.thy
 changeset 47108 2a1953f0d20d parent 42463 f270e3e18be5 child 53015 a1119cf551e8
```     1.1 --- a/src/HOL/ex/Groebner_Examples.thy	Sat Mar 24 16:27:04 2012 +0100
1.2 +++ b/src/HOL/ex/Groebner_Examples.thy	Sun Mar 25 20:15:39 2012 +0200
1.3 @@ -31,7 +31,7 @@
1.4      (Conv.arg_conv (Conv.arg1_conv (Semiring_Normalizer.semiring_normalize_conv @{context})))) *})
1.5    by (rule refl)
1.6
1.7 -lemma "((-3) ^ (Suc (Suc (Suc 0)))) == (X::'a::{number_ring})"
1.8 +lemma "((-3) ^ (Suc (Suc (Suc 0)))) == (X::'a::{comm_ring_1})"
1.9    apply (simp only: power_Suc power_0)
1.10    apply (simp only: semiring_norm)
1.11    oops
1.12 @@ -58,7 +58,7 @@
1.13    by algebra
1.14
1.15  lemma
1.16 -  fixes x::"'a::{idom,number_ring}"
1.17 +  fixes x::"'a::{idom}"
1.18    shows "x^2*y = x^2 & x*y^2 = y^2 \<longleftrightarrow>  x=1 & y=1 | x=0 & y=0"
1.19    by algebra
1.20
1.21 @@ -69,7 +69,7 @@
1.22    "sq x == x*x"
1.23
1.24  lemma
1.25 -  fixes x1 :: "'a::{idom,number_ring}"
1.26 +  fixes x1 :: "'a::{idom}"
1.27    shows
1.28    "(sq x1 + sq x2 + sq x3 + sq x4) * (sq y1 + sq y2 + sq y3 + sq y4) =
1.29      sq (x1*y1 - x2*y2 - x3*y3 - x4*y4)  +
1.30 @@ -79,7 +79,7 @@