--- a/src/HOL/ex/Groebner_Examples.thy Tue Apr 28 19:15:50 2009 +0200
+++ b/src/HOL/ex/Groebner_Examples.thy Wed Apr 29 14:20:26 2009 +0200
@@ -1,5 +1,4 @@
(* Title: HOL/ex/Groebner_Examples.thy
- ID: $Id$
Author: Amine Chaieb, TU Muenchen
*)
@@ -11,7 +10,7 @@
subsection {* Basic examples *}
-lemma "3 ^ 3 == (?X::'a::{number_ring,recpower})"
+lemma "3 ^ 3 == (?X::'a::{number_ring})"
by sring_norm
lemma "(x - (-2))^5 == ?X::int"
@@ -20,7 +19,7 @@
lemma "(x - (-2))^5 * (y - 78) ^ 8 == ?X::int"
by sring_norm
-lemma "((-3) ^ (Suc (Suc (Suc 0)))) == (X::'a::{number_ring,recpower})"
+lemma "((-3) ^ (Suc (Suc (Suc 0)))) == (X::'a::{number_ring})"
apply (simp only: power_Suc power_0)
apply (simp only: comp_arith)
oops
@@ -47,7 +46,7 @@
by algebra
lemma
- fixes x::"'a::{idom,recpower,number_ring}"
+ fixes x::"'a::{idom,number_ring}"
shows "x^2*y = x^2 & x*y^2 = y^2 \<longleftrightarrow> x=1 & y=1 | x=0 & y=0"
by algebra
@@ -58,7 +57,7 @@
"sq x == x*x"
lemma
- fixes x1 :: "'a::{idom,recpower,number_ring}"
+ fixes x1 :: "'a::{idom,number_ring}"
shows
"(sq x1 + sq x2 + sq x3 + sq x4) * (sq y1 + sq y2 + sq y3 + sq y4) =
sq (x1*y1 - x2*y2 - x3*y3 - x4*y4) +
@@ -68,7 +67,7 @@
by (algebra add: sq_def)
lemma
- fixes p1 :: "'a::{idom,recpower,number_ring}"
+ fixes p1 :: "'a::{idom,number_ring}"
shows
"(sq p1 + sq q1 + sq r1 + sq s1 + sq t1 + sq u1 + sq v1 + sq w1) *
(sq p2 + sq q2 + sq r2 + sq s2 + sq t2 + sq u2 + sq v2 + sq w2)