# HG changeset patch
# User haftmann
# Date 1241007626 -7200
# Node ID 53642251a04f803654b000d6962c679edc87a17d
# Parent  9999a77590c368bcd203f32d3f194b49a81da082
farewell to class recpower

diff -r 9999a77590c3 -r 53642251a04f src/HOL/Algebra/poly/UnivPoly2.thy
--- a/src/HOL/Algebra/poly/UnivPoly2.thy	Tue Apr 28 19:15:50 2009 +0200
+++ b/src/HOL/Algebra/poly/UnivPoly2.thy	Wed Apr 29 14:20:26 2009 +0200
@@ -347,9 +347,6 @@
     by (simp add: up_divide_def)
 qed
 
-instance up :: (ring) recpower proof
-qed simp_all
-
 (* Further properties of monom *)
 
 lemma monom_zero [simp]:
diff -r 9999a77590c3 -r 53642251a04f src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Tue Apr 28 19:15:50 2009 +0200
+++ b/src/HOL/Complex.thy	Wed Apr 29 14:20:26 2009 +0200
@@ -157,11 +157,6 @@
 end
 
 
-subsection {* Exponentiation *}
-
-instance complex :: recpower ..
-
-
 subsection {* Numerals and Arithmetic *}
 
 instantiation complex :: number_ring
diff -r 9999a77590c3 -r 53642251a04f src/HOL/Decision_Procs/Dense_Linear_Order.thy
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Tue Apr 28 19:15:50 2009 +0200
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Wed Apr 29 14:20:26 2009 +0200
@@ -639,7 +639,7 @@
 
 interpretation class_ordered_field_dense_linear_order: constr_dense_linear_order
  "op <=" "op <"
-   "\<lambda> x y. 1/2 * ((x::'a::{ordered_field,recpower,number_ring}) + y)"
+   "\<lambda> x y. 1/2 * ((x::'a::{ordered_field,number_ring}) + y)"
 proof (unfold_locales, dlo, dlo, auto)
   fix x y::'a assume lt: "x < y"
   from  less_half_sum[OF lt] show "x < (x + y) /2" by simp
diff -r 9999a77590c3 -r 53642251a04f src/HOL/Decision_Procs/ex/Dense_Linear_Order_Ex.thy
--- a/src/HOL/Decision_Procs/ex/Dense_Linear_Order_Ex.thy	Tue Apr 28 19:15:50 2009 +0200
+++ b/src/HOL/Decision_Procs/ex/Dense_Linear_Order_Ex.thy	Wed Apr 29 14:20:26 2009 +0200
@@ -7,147 +7,147 @@
 begin
 
 lemma
-  "\<exists>(y::'a::{ordered_field,recpower,number_ring, division_by_zero}) <2. x + 3* y < 0 \<and> x - y >0"
+  "\<exists>(y::'a::{ordered_field,number_ring, division_by_zero}) <2. x + 3* y < 0 \<and> x - y >0"
   by ferrack
 
-lemma "~ (ALL x (y::'a::{ordered_field,recpower,number_ring, division_by_zero}). x < y --> 10*x < 11*y)"
+lemma "~ (ALL x (y::'a::{ordered_field,number_ring, division_by_zero}). x < y --> 10*x < 11*y)"
   by ferrack
 
-lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. x < y --> (10*(x + 5*y + -1) < 60*y)"
+lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}) y. x < y --> (10*(x + 5*y + -1) < 60*y)"
   by ferrack
 
-lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. x ~= y --> x < y"
+lemma "EX (x::'a::{ordered_field,number_ring, division_by_zero}) y. x ~= y --> x < y"
   by ferrack
 
-lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (x ~= y & 10*x ~= 9*y & 10*x < y) --> x < y"
+lemma "EX (x::'a::{ordered_field,number_ring, division_by_zero}) y. (x ~= y & 10*x ~= 9*y & 10*x < y) --> x < y"
   by ferrack
 
-lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (x ~= y & 5*x <= y) --> 500*x <= 100*y"
+lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}) y. (x ~= y & 5*x <= y) --> 500*x <= 100*y"
   by ferrack
 
-lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (EX (y::'a::{ordered_field,recpower,number_ring, division_by_zero}). 4*x + 3*y <= 0 & 4*x + 3*y >= -1)"
+lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}). (EX (y::'a::{ordered_field,number_ring, division_by_zero}). 4*x + 3*y <= 0 & 4*x + 3*y >= -1)"
   by ferrack
 
-lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) < 0. (EX (y::'a::{ordered_field,recpower,number_ring, division_by_zero}) > 0. 7*x + y > 0 & x - y <= 9)"
+lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}) < 0. (EX (y::'a::{ordered_field,number_ring, division_by_zero}) > 0. 7*x + y > 0 & x - y <= 9)"
   by ferrack
 
-lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (0 < x & x < 1) --> (ALL y > 1. x + y ~= 1)"
+lemma "EX (x::'a::{ordered_field,number_ring, division_by_zero}). (0 < x & x < 1) --> (ALL y > 1. x + y ~= 1)"
   by ferrack
 
-lemma "EX x. (ALL (y::'a::{ordered_field,recpower,number_ring, division_by_zero}). y < 2 -->  2*(y - x) \<le> 0 )"
+lemma "EX x. (ALL (y::'a::{ordered_field,number_ring, division_by_zero}). y < 2 -->  2*(y - x) \<le> 0 )"
   by ferrack
 
-lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). x < 10 | x > 20 | (EX y. y>= 0 & y <= 10 & x+y = 20)"
+lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}). x < 10 | x > 20 | (EX y. y>= 0 & y <= 10 & x+y = 20)"
   by ferrack
 
-lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z. x + y < z --> y >= z --> x < 0"
+lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}) y z. x + y < z --> y >= z --> x < 0"
   by ferrack
 
-lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z. x + 7*y < 5* z & 5*y >= 7*z & x < 0"
+lemma "EX (x::'a::{ordered_field,number_ring, division_by_zero}) y z. x + 7*y < 5* z & 5*y >= 7*z & x < 0"
   by ferrack
 
-lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z. abs (x + y) <= z --> (abs z = z)"
+lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}) y z. abs (x + y) <= z --> (abs z = z)"
   by ferrack
 
-lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z. x + 7*y - 5* z < 0 & 5*y + 7*z + 3*x < 0"
+lemma "EX (x::'a::{ordered_field,number_ring, division_by_zero}) y z. x + 7*y - 5* z < 0 & 5*y + 7*z + 3*x < 0"
   by ferrack
 
-lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z. (abs (5*x+3*y+z) <= 5*x+3*y+z & abs (5*x+3*y+z) >= - (5*x+3*y+z)) | (abs (5*x+3*y+z) >= 5*x+3*y+z & abs (5*x+3*y+z) <= - (5*x+3*y+z))"
+lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}) y z. (abs (5*x+3*y+z) <= 5*x+3*y+z & abs (5*x+3*y+z) >= - (5*x+3*y+z)) | (abs (5*x+3*y+z) >= 5*x+3*y+z & abs (5*x+3*y+z) <= - (5*x+3*y+z))"
   by ferrack
 
-lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. x < y --> (EX z>0. x+z = y)"
+lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}) y. x < y --> (EX z>0. x+z = y)"
   by ferrack
 
-lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. x < y --> (EX z>0. x+z = y)"
+lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}) y. x < y --> (EX z>0. x+z = y)"
   by ferrack
 
-lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (EX z>0. abs (x - y) <= z )"
+lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}) y. (EX z>0. abs (x - y) <= z )"
   by ferrack
 
-lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (ALL z<0. (z < x --> z <= y) & (z > y --> z >= x))"
+lemma "EX (x::'a::{ordered_field,number_ring, division_by_zero}) y. (ALL z<0. (z < x --> z <= y) & (z > y --> z >= x))"
   by ferrack
 
-lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (ALL z>=0. abs (3*x+7*y) <= 2*z + 1)"
+lemma "EX (x::'a::{ordered_field,number_ring, division_by_zero}) y. (ALL z>=0. abs (3*x+7*y) <= 2*z + 1)"
   by ferrack
 
-lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (ALL z<0. (z < x --> z <= y) & (z > y --> z >= x))"
+lemma "EX (x::'a::{ordered_field,number_ring, division_by_zero}) y. (ALL z<0. (z < x --> z <= y) & (z > y --> z >= x))"
   by ferrack
 
-lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero})>0. (ALL y. (EX z. 13* abs z \<noteq> abs (12*y - x) & 5*x - 3*(abs y) <= 7*z))"
+lemma "EX (x::'a::{ordered_field,number_ring, division_by_zero})>0. (ALL y. (EX z. 13* abs z \<noteq> abs (12*y - x) & 5*x - 3*(abs y) <= 7*z))"
   by ferrack
 
-lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). abs (4*x + 17) < 4 & (ALL y . abs (x*34 - 34*y - 9) \<noteq> 0 \<longrightarrow> (EX z. 5*x - 3*abs y <= 7*z))"
+lemma "EX (x::'a::{ordered_field,number_ring, division_by_zero}). abs (4*x + 17) < 4 & (ALL y . abs (x*34 - 34*y - 9) \<noteq> 0 \<longrightarrow> (EX z. 5*x - 3*abs y <= 7*z))"
   by ferrack
 
-lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (EX y > abs (23*x - 9). (ALL z > abs (3*y - 19* abs x). x+z > 2*y))"
+lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}). (EX y > abs (23*x - 9). (ALL z > abs (3*y - 19* abs x). x+z > 2*y))"
   by ferrack
 
-lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (EX y< abs (3*x - 1). (ALL z >= (3*abs x - 1). abs (12*x - 13*y + 19*z) > abs (23*x) ))"
+lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}). (EX y< abs (3*x - 1). (ALL z >= (3*abs x - 1). abs (12*x - 13*y + 19*z) > abs (23*x) ))"
   by ferrack
 
-lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). abs x < 100 & (ALL y > x. (EX z<2*y - x. 5*x - 3*y <= 7*z))"
+lemma "EX (x::'a::{ordered_field,number_ring, division_by_zero}). abs x < 100 & (ALL y > x. (EX z<2*y - x. 5*x - 3*y <= 7*z))"
   by ferrack
 
-lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z w. 7*x<3*y --> 5*y < 7*z --> z < 2*w --> 7*(2*w-x) > 2*y"
+lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}) y z w. 7*x<3*y --> 5*y < 7*z --> z < 2*w --> 7*(2*w-x) > 2*y"
   by ferrack
 
-lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z w. 5*x + 3*z - 17*w + abs (y - 8*x + z) <= 89"
+lemma "EX (x::'a::{ordered_field,number_ring, division_by_zero}) y z w. 5*x + 3*z - 17*w + abs (y - 8*x + z) <= 89"
   by ferrack
 
-lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z w. 5*x + 3*z - 17*w + 7* (y - 8*x + z) <= max y (7*z - x + w)"
+lemma "EX (x::'a::{ordered_field,number_ring, division_by_zero}) y z w. 5*x + 3*z - 17*w + 7* (y - 8*x + z) <= max y (7*z - x + w)"
   by ferrack
 
-lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w)"
+lemma "EX (x::'a::{ordered_field,number_ring, division_by_zero}) y z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w)"
   by ferrack
 
-lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z. (EX w >= (x+y+z). w <= abs x + abs y + abs z)"
+lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}) y z. (EX w >= (x+y+z). w <= abs x + abs y + abs z)"
   by ferrack
 
-lemma "~(ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (EX y z w. 3* x + z*4 = 3*y & x + y < z & x> w & 3*x < w + y))"
+lemma "~(ALL (x::'a::{ordered_field,number_ring, division_by_zero}). (EX y z w. 3* x + z*4 = 3*y & x + y < z & x> w & 3*x < w + y))"
   by ferrack
 
-lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (EX z w. abs (x-y) = (z-w) & z*1234 < 233*x & w ~= y)"
+lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}) y. (EX z w. abs (x-y) = (z-w) & z*1234 < 233*x & w ~= y)"
   by ferrack
 
-lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (EX y z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w))"
+lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}). (EX y z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w))"
   by ferrack
 
-lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z. (ALL w >= abs (x+y+z). w >= abs x + abs y + abs z)"
+lemma "EX (x::'a::{ordered_field,number_ring, division_by_zero}) y z. (ALL w >= abs (x+y+z). w >= abs x + abs y + abs z)"
   by ferrack
 
-lemma "EX z. (ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (EX w >= (x+y+z). w <= abs x + abs y + abs z))"
+lemma "EX z. (ALL (x::'a::{ordered_field,number_ring, division_by_zero}) y. (EX w >= (x+y+z). w <= abs x + abs y + abs z))"
   by ferrack
 
-lemma "EX z. (ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) < abs z. (EX y w. x< y & x < z & x> w & 3*x < w + y))"
+lemma "EX z. (ALL (x::'a::{ordered_field,number_ring, division_by_zero}) < abs z. (EX y w. x< y & x < z & x> w & 3*x < w + y))"
   by ferrack
 
-lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (EX z. (ALL w. abs (x-y) = abs (z-w) --> z < x & w ~= y))"
+lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}) y. (EX z. (ALL w. abs (x-y) = abs (z-w) --> z < x & w ~= y))"
   by ferrack
 
-lemma "EX y. (ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (EX z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w)))"
+lemma "EX y. (ALL (x::'a::{ordered_field,number_ring, division_by_zero}). (EX z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w)))"
   by ferrack
 
-lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) z. (ALL w >= 13*x - 4*z. (EX y. w >= abs x + abs y + z))"
+lemma "EX (x::'a::{ordered_field,number_ring, division_by_zero}) z. (ALL w >= 13*x - 4*z. (EX y. w >= abs x + abs y + z))"
   by ferrack
 
-lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (ALL y < x. (EX z > (x+y).
+lemma "EX (x::'a::{ordered_field,number_ring, division_by_zero}). (ALL y < x. (EX z > (x+y).
   (ALL w. 5*w + 10*x - z >= y --> w + 7*x + 3*z >= 2*y)))"
   by ferrack
 
-lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (ALL y. (EX z > y.
+lemma "EX (x::'a::{ordered_field,number_ring, division_by_zero}). (ALL y. (EX z > y.
   (ALL w . w < 13 --> w + 10*x - z >= y --> 5*w + 7*x + 13*z >= 2*y)))"
   by ferrack
 
-lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w)"
+lemma "EX (x::'a::{ordered_field,number_ring, division_by_zero}) y z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w)"
   by ferrack
 
-lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (EX y. (ALL z>19. y <= x + z & (EX w. abs (y - x) < w)))"
+lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}). (EX y. (ALL z>19. y <= x + z & (EX w. abs (y - x) < w)))"
   by ferrack
 
-lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (EX y. (ALL z>19. y <= x + z & (EX w. abs (x + z) < w - y)))"
+lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}). (EX y. (ALL z>19. y <= x + z & (EX w. abs (x + z) < w - y)))"
   by ferrack
 
-lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (EX y. abs y ~= abs x & (ALL z> max x y. (EX w. w ~= y & w ~= z & 3*w - z >= x + y)))"
+lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}). (EX y. abs y ~= abs x & (ALL z> max x y. (EX w. w ~= y & w ~= z & 3*w - z >= x + y)))"
   by ferrack
 
 end
diff -r 9999a77590c3 -r 53642251a04f src/HOL/Int.thy
--- a/src/HOL/Int.thy	Tue Apr 28 19:15:50 2009 +0200
+++ b/src/HOL/Int.thy	Wed Apr 29 14:20:26 2009 +0200
@@ -2178,8 +2178,6 @@
 
 subsection {* Legacy theorems *}
 
-instance int :: recpower ..
-
 lemmas zminus_zminus = minus_minus [of "z::int", standard]
 lemmas zminus_0 = minus_zero [where 'a=int]
 lemmas zminus_zadd_distrib = minus_add_distrib [of "z::int" "w", standard]
diff -r 9999a77590c3 -r 53642251a04f src/HOL/Library/Binomial.thy
--- a/src/HOL/Library/Binomial.thy	Tue Apr 28 19:15:50 2009 +0200
+++ b/src/HOL/Library/Binomial.thy	Wed Apr 29 14:20:26 2009 +0200
@@ -292,7 +292,7 @@
 
 subsection{* Generalized binomial coefficients *}
 
-definition gbinomial :: "'a::{field, recpower,ring_char_0} \<Rightarrow> nat \<Rightarrow> 'a" (infixl "gchoose" 65)
+definition gbinomial :: "'a::{field, ring_char_0} \<Rightarrow> nat \<Rightarrow> 'a" (infixl "gchoose" 65)
   where "a gchoose n = (if n = 0 then 1 else (setprod (\<lambda>i. a - of_nat i) {0 .. n - 1}) / of_nat (fact n))"
 
 lemma gbinomial_0[simp]: "a gchoose 0 = 1" "0 gchoose (Suc n) = 0"
@@ -420,16 +420,16 @@
   by (simp add: gbinomial_def)
  
 lemma gbinomial_mult_fact:
-  "(of_nat (fact (Suc k)) :: 'a) * ((a::'a::{field, ring_char_0,recpower}) gchoose (Suc k)) = (setprod (\<lambda>i. a - of_nat i) {0 .. k})"
+  "(of_nat (fact (Suc k)) :: 'a) * ((a::'a::{field, ring_char_0}) gchoose (Suc k)) = (setprod (\<lambda>i. a - of_nat i) {0 .. k})"
   unfolding gbinomial_Suc
   by (simp_all add: field_simps del: fact_Suc)
 
 lemma gbinomial_mult_fact':
-  "((a::'a::{field, ring_char_0,recpower}) gchoose (Suc k)) * (of_nat (fact (Suc k)) :: 'a) = (setprod (\<lambda>i. a - of_nat i) {0 .. k})"
+  "((a::'a::{field, ring_char_0}) gchoose (Suc k)) * (of_nat (fact (Suc k)) :: 'a) = (setprod (\<lambda>i. a - of_nat i) {0 .. k})"
   using gbinomial_mult_fact[of k a]
   apply (subst mult_commute) .
 
-lemma gbinomial_Suc_Suc: "((a::'a::{field,recpower, ring_char_0}) + 1) gchoose (Suc k) = a gchoose k + (a gchoose (Suc k))"
+lemma gbinomial_Suc_Suc: "((a::'a::{field, ring_char_0}) + 1) gchoose (Suc k) = a gchoose k + (a gchoose (Suc k))"
 proof-
   {assume "k = 0" then have ?thesis by simp}
   moreover
diff -r 9999a77590c3 -r 53642251a04f src/HOL/Library/Commutative_Ring.thy
--- a/src/HOL/Library/Commutative_Ring.thy	Tue Apr 28 19:15:50 2009 +0200
+++ b/src/HOL/Library/Commutative_Ring.thy	Wed Apr 29 14:20:26 2009 +0200
@@ -27,15 +27,15 @@
 
 text {* Interpretation functions for the shadow syntax. *}
 
-fun
-  Ipol :: "'a::{comm_ring,recpower} list \<Rightarrow> 'a pol \<Rightarrow> 'a"
+primrec
+  Ipol :: "'a::{comm_ring_1} list \<Rightarrow> 'a pol \<Rightarrow> 'a"
 where
     "Ipol l (Pc c) = c"
   | "Ipol l (Pinj i P) = Ipol (drop i l) P"
   | "Ipol l (PX P x Q) = Ipol l P * (hd l)^x + Ipol (drop 1 l) Q"
 
-fun
-  Ipolex :: "'a::{comm_ring,recpower} list \<Rightarrow> 'a polex \<Rightarrow> 'a"
+primrec
+  Ipolex :: "'a::{comm_ring_1} list \<Rightarrow> 'a polex \<Rightarrow> 'a"
 where
     "Ipolex l (Pol P) = Ipol l P"
   | "Ipolex l (Add P Q) = Ipolex l P + Ipolex l Q"
@@ -54,7 +54,7 @@
     PX p1 y p2 \<Rightarrow> Pinj x P)"
 
 definition
-  mkPX :: "'a::{comm_ring,recpower} pol \<Rightarrow> nat \<Rightarrow> 'a pol \<Rightarrow> 'a pol" where
+  mkPX :: "'a::{comm_ring} pol \<Rightarrow> nat \<Rightarrow> 'a pol \<Rightarrow> 'a pol" where
   "mkPX P i Q = (case P of
     Pc c \<Rightarrow> (if (c = 0) then (mkPinj 1 Q) else (PX P i Q)) |
     Pinj j R \<Rightarrow> PX P i Q |
@@ -63,7 +63,7 @@
 text {* Defining the basic ring operations on normalized polynomials *}
 
 function
-  add :: "'a::{comm_ring,recpower} pol \<Rightarrow> 'a pol \<Rightarrow> 'a pol" (infixl "\<oplus>" 65)
+  add :: "'a::{comm_ring} pol \<Rightarrow> 'a pol \<Rightarrow> 'a pol" (infixl "\<oplus>" 65)
 where
     "Pc a \<oplus> Pc b = Pc (a + b)"
   | "Pc c \<oplus> Pinj i P = Pinj i (P \<oplus> Pc c)"
@@ -90,7 +90,7 @@
 termination by (relation "measure (\<lambda>(x, y). size x + size y)") auto
 
 function
-  mul :: "'a::{comm_ring,recpower} pol \<Rightarrow> 'a pol \<Rightarrow> 'a pol" (infixl "\<otimes>" 70)
+  mul :: "'a::{comm_ring} pol \<Rightarrow> 'a pol \<Rightarrow> 'a pol" (infixl "\<otimes>" 70)
 where
     "Pc a \<otimes> Pc b = Pc (a * b)"
   | "Pc c \<otimes> Pinj i P =
@@ -122,8 +122,8 @@
   (auto simp add: mkPinj_def split: pol.split)
 
 text {* Negation*}
-fun
-  neg :: "'a::{comm_ring,recpower} pol \<Rightarrow> 'a pol"
+primrec
+  neg :: "'a::{comm_ring} pol \<Rightarrow> 'a pol"
 where
     "neg (Pc c) = Pc (-c)"
   | "neg (Pinj i P) = Pinj i (neg P)"
@@ -131,13 +131,13 @@
 
 text {* Substraction *}
 definition
-  sub :: "'a::{comm_ring,recpower} pol \<Rightarrow> 'a pol \<Rightarrow> 'a pol" (infixl "\<ominus>" 65)
+  sub :: "'a::{comm_ring} pol \<Rightarrow> 'a pol \<Rightarrow> 'a pol" (infixl "\<ominus>" 65)
 where
   "sub P Q = P \<oplus> neg Q"
 
 text {* Square for Fast Exponentation *}
-fun
-  sqr :: "'a::{comm_ring,recpower} pol \<Rightarrow> 'a pol"
+primrec
+  sqr :: "'a::{comm_ring_1} pol \<Rightarrow> 'a pol"
 where
     "sqr (Pc c) = Pc (c * c)"
   | "sqr (Pinj i P) = mkPinj i (sqr P)"
@@ -146,7 +146,7 @@
 
 text {* Fast Exponentation *}
 fun
-  pow :: "nat \<Rightarrow> 'a::{comm_ring,recpower} pol \<Rightarrow> 'a pol"
+  pow :: "nat \<Rightarrow> 'a::{comm_ring_1} pol \<Rightarrow> 'a pol"
 where
     "pow 0 P = Pc 1"
   | "pow n P = (if even n then pow (n div 2) (sqr P)
@@ -161,8 +161,8 @@
 
 text {* Normalization of polynomial expressions *}
 
-fun
-  norm :: "'a::{comm_ring,recpower} polex \<Rightarrow> 'a pol"
+primrec
+  norm :: "'a::{comm_ring_1} polex \<Rightarrow> 'a pol"
 where
     "norm (Pol P) = P"
   | "norm (Add P Q) = norm P \<oplus> norm Q"
diff -r 9999a77590c3 -r 53642251a04f src/HOL/Library/Euclidean_Space.thy
--- a/src/HOL/Library/Euclidean_Space.thy	Tue Apr 28 19:15:50 2009 +0200
+++ b/src/HOL/Library/Euclidean_Space.thy	Wed Apr 29 14:20:26 2009 +0200
@@ -253,8 +253,6 @@
   "vector_power x 0 = 1"
   | "vector_power x (Suc n) = x * vector_power x n"
 
-instance "^" :: (recpower,type) recpower ..
-
 instance "^" :: (semiring,type) semiring
   apply (intro_classes) by (vector ring_simps)+
 
@@ -2757,7 +2755,7 @@
 (* Geometric progression.                                                    *)
 (* ------------------------------------------------------------------------- *)
 
-lemma sum_gp_basic: "((1::'a::{field, recpower}) - x) * setsum (\<lambda>i. x^i) {0 .. n} = (1 - x^(Suc n))"
+lemma sum_gp_basic: "((1::'a::{field}) - x) * setsum (\<lambda>i. x^i) {0 .. n} = (1 - x^(Suc n))"
   (is "?lhs = ?rhs")
 proof-
   {assume x1: "x = 1" hence ?thesis by simp}
@@ -2775,7 +2773,7 @@
 qed
 
 lemma sum_gp_multiplied: assumes mn: "m <= n"
-  shows "((1::'a::{field, recpower}) - x) * setsum (op ^ x) {m..n} = x^m - x^ Suc n"
+  shows "((1::'a::{field}) - x) * setsum (op ^ x) {m..n} = x^m - x^ Suc n"
   (is "?lhs = ?rhs")
 proof-
   let ?S = "{0..(n - m)}"
@@ -2792,7 +2790,7 @@
     by (simp add: ring_simps power_add[symmetric])
 qed
 
-lemma sum_gp: "setsum (op ^ (x::'a::{field, recpower})) {m .. n} =
+lemma sum_gp: "setsum (op ^ (x::'a::{field})) {m .. n} =
    (if n < m then 0 else if x = 1 then of_nat ((n + 1) - m)
                     else (x^ m - x^ (Suc n)) / (1 - x))"
 proof-
@@ -2808,7 +2806,7 @@
   ultimately show ?thesis by metis
 qed
 
-lemma sum_gp_offset: "setsum (op ^ (x::'a::{field,recpower})) {m .. m+n} =
+lemma sum_gp_offset: "setsum (op ^ (x::'a::{field})) {m .. m+n} =
   (if x = 1 then of_nat n + 1 else x^m * (1 - x^Suc n) / (1 - x))"
   unfolding sum_gp[of x m "m + n"] power_Suc
   by (simp add: ring_simps power_add)
diff -r 9999a77590c3 -r 53642251a04f src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Tue Apr 28 19:15:50 2009 +0200
+++ b/src/HOL/Library/Float.thy	Wed Apr 29 14:20:26 2009 +0200
@@ -443,8 +443,6 @@
 lemma Ifloat_min: "Ifloat (min x y) = min (Ifloat x) (Ifloat y)" unfolding min_def le_float_def by auto
 lemma Ifloat_max: "Ifloat (max a b) = max (Ifloat a) (Ifloat b)" unfolding max_def le_float_def by auto
 
-instance float :: recpower ..
-
 lemma float_power: "Ifloat (x ^ n) = Ifloat x ^ n"
   by (induct n) simp_all
 
diff -r 9999a77590c3 -r 53642251a04f src/HOL/Library/Formal_Power_Series.thy
--- a/src/HOL/Library/Formal_Power_Series.thy	Tue Apr 28 19:15:50 2009 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy	Wed Apr 29 14:20:26 2009 +0200
@@ -680,8 +680,6 @@
 
 subsection {* Powers*}
 
-instance fps :: (semiring_1) recpower ..
-
 lemma fps_power_zeroth_eq_one: "a$0 =1 \<Longrightarrow> a^n $ 0 = (1::'a::semiring_1)"
   by (induct n, auto simp add: expand_fps_eq fps_mult_nth)
 
@@ -701,11 +699,11 @@
 lemma startsby_zero_power:"a $0 = (0::'a::comm_ring_1) \<Longrightarrow> n > 0 \<Longrightarrow> a^n $0 = 0"
   by (induct n, auto simp add: fps_mult_nth)
 
-lemma startsby_power:"a $0 = (v::'a::{comm_ring_1, recpower}) \<Longrightarrow> a^n $0 = v^n"
+lemma startsby_power:"a $0 = (v::'a::{comm_ring_1}) \<Longrightarrow> a^n $0 = v^n"
   by (induct n, auto simp add: fps_mult_nth power_Suc)
 
 lemma startsby_zero_power_iff[simp]:
-  "a^n $0 = (0::'a::{idom, recpower}) \<longleftrightarrow> (n \<noteq> 0 \<and> a$0 = 0)"
+  "a^n $0 = (0::'a::{idom}) \<longleftrightarrow> (n \<noteq> 0 \<and> a$0 = 0)"
 apply (rule iffI)
 apply (induct n, auto simp add: power_Suc fps_mult_nth)
 by (rule startsby_zero_power, simp_all)
@@ -748,7 +746,7 @@
   apply (rule startsby_zero_power_prefix[rule_format, OF a0])
   by arith
 
-lemma startsby_zero_power_nth_same: assumes a0: "a$0 = (0::'a::{recpower, idom})"
+lemma startsby_zero_power_nth_same: assumes a0: "a$0 = (0::'a::{idom})"
   shows "a^n $ n = (a$1) ^ n"
 proof(induct n)
   case 0 thus ?case by (simp add: power_0)
@@ -769,7 +767,7 @@
 qed
 
 lemma fps_inverse_power:
-  fixes a :: "('a::{field, recpower}) fps"
+  fixes a :: "('a::{field}) fps"
   shows "inverse (a^n) = inverse a ^ n"
 proof-
   {assume a0: "a$0 = 0"
@@ -858,7 +856,7 @@
 
 subsection{* The eXtractor series X*}
 
-lemma minus_one_power_iff: "(- (1::'a :: {recpower, comm_ring_1})) ^ n = (if even n then 1 else - 1)"
+lemma minus_one_power_iff: "(- (1::'a :: {comm_ring_1})) ^ n = (if even n then 1 else - 1)"
   by (induct n, auto)
 
 definition "X = Abs_fps (\<lambda>n. if n = 1 then 1 else 0)"
@@ -915,7 +913,7 @@
   by (simp add: X_power_iff)
 
 lemma fps_inverse_X_plus1:
-  "inverse (1 + X) = Abs_fps (\<lambda>n. (- (1::'a::{recpower, field})) ^ n)" (is "_ = ?r")
+  "inverse (1 + X) = Abs_fps (\<lambda>n. (- (1::'a::{field})) ^ n)" (is "_ = ?r")
 proof-
   have eq: "(1 + X) * ?r = 1"
     unfolding minus_one_power_iff
@@ -1014,7 +1012,7 @@
 
 
 lemma fps_mult_XD_shift:
-  "(XD ^^ k) (a:: ('a::{comm_ring_1, recpower}) fps) = Abs_fps (\<lambda>n. (of_nat n ^ k) * a$n)"
+  "(XD ^^ k) (a:: ('a::{comm_ring_1}) fps) = Abs_fps (\<lambda>n. (of_nat n ^ k) * a$n)"
   by (induct k arbitrary: a) (simp_all add: power_Suc XD_def fps_eq_iff ring_simps del: One_nat_def)
 
 subsubsection{* Rule 3 is trivial and is given by @{text fps_times_def}*}
@@ -1296,7 +1294,7 @@
   by (cases m, simp_all add: fps_power_nth_Suc del: power_Suc)
 
 lemma fps_nth_power_0:
-  fixes m :: nat and a :: "('a::{comm_ring_1, recpower}) fps"
+  fixes m :: nat and a :: "('a::{comm_ring_1}) fps"
   shows "(a ^m)$0 = (a$0) ^ m"
 proof-
   {assume "m=0" hence ?thesis by simp}
@@ -1312,7 +1310,7 @@
 qed
 
 lemma fps_compose_inj_right:
-  assumes a0: "a$0 = (0::'a::{recpower,idom})"
+  assumes a0: "a$0 = (0::'a::{idom})"
   and a1: "a$1 \<noteq> 0"
   shows "(b oo a = c oo a) \<longleftrightarrow> b = c" (is "?lhs \<longleftrightarrow>?rhs")
 proof-
@@ -1353,7 +1351,7 @@
 subsection {* Radicals *}
 
 declare setprod_cong[fundef_cong]
-function radical :: "(nat \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> ('a::{field, recpower}) fps \<Rightarrow> nat \<Rightarrow> 'a" where
+function radical :: "(nat \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> ('a::{field}) fps \<Rightarrow> nat \<Rightarrow> 'a" where
   "radical r 0 a 0 = 1"
 | "radical r 0 a (Suc n) = 0"
 | "radical r (Suc k) a 0 = r (Suc k) (a$0)"
@@ -1441,7 +1439,7 @@
 qed
 
 lemma power_radical:
-  fixes a:: "'a ::{field, ring_char_0, recpower} fps"
+  fixes a:: "'a ::{field, ring_char_0} fps"
   assumes r0: "(r (Suc k) (a$0)) ^ Suc k = a$0" and a0: "a$0 \<noteq> 0"
   shows "(fps_radical r (Suc k) a) ^ (Suc k) = a"
 proof-
@@ -1502,7 +1500,7 @@
 
 lemma radical_unique:
   assumes r0: "(r (Suc k) (b$0)) ^ Suc k = b$0"
-  and a0: "r (Suc k) (b$0 ::'a::{field, ring_char_0, recpower}) = a$0" and b0: "b$0 \<noteq> 0"
+  and a0: "r (Suc k) (b$0 ::'a::{field, ring_char_0}) = a$0" and b0: "b$0 \<noteq> 0"
   shows "a^(Suc k) = b \<longleftrightarrow> a = fps_radical r (Suc k) b"
 proof-
   let ?r = "fps_radical r (Suc k) b"
@@ -1597,7 +1595,7 @@
 
 lemma radical_power:
   assumes r0: "r (Suc k) ((a$0) ^ Suc k) = a$0"
-  and a0: "(a$0 ::'a::{field, ring_char_0, recpower}) \<noteq> 0"
+  and a0: "(a$0 ::'a::{field, ring_char_0}) \<noteq> 0"
   shows "(fps_radical r (Suc k) (a ^ Suc k)) = a"
 proof-
   let ?ak = "a^ Suc k"
@@ -1609,7 +1607,7 @@
 qed
 
 lemma fps_deriv_radical:
-  fixes a:: "'a ::{field, ring_char_0, recpower} fps"
+  fixes a:: "'a ::{field, ring_char_0} fps"
   assumes r0: "(r (Suc k) (a$0)) ^ Suc k = a$0" and a0: "a$0 \<noteq> 0"
   shows "fps_deriv (fps_radical r (Suc k) a) = fps_deriv a / (fps_const (of_nat (Suc k)) * (fps_radical r (Suc k) a) ^ k)"
 proof-
@@ -1630,7 +1628,7 @@
 qed
 
 lemma radical_mult_distrib:
-  fixes a:: "'a ::{field, ring_char_0, recpower} fps"
+  fixes a:: "'a ::{field, ring_char_0} fps"
   assumes
   ra0: "r (k) (a $ 0) ^ k = a $ 0"
   and rb0: "r (k) (b $ 0) ^ k = b $ 0"
@@ -1656,7 +1654,7 @@
 qed
 
 lemma radical_inverse:
-  fixes a:: "'a ::{field, ring_char_0, recpower} fps"
+  fixes a:: "'a ::{field, ring_char_0} fps"
   assumes
   ra0: "r (k) (a $ 0) ^ k = a $ 0"
   and ria0: "r (k) (inverse (a $ 0)) = inverse (r (k) (a $ 0))"
@@ -1698,7 +1696,7 @@
   by (simp add: fps_divide_def)
 
 lemma radical_divide:
-  fixes a:: "'a ::{field, ring_char_0, recpower} fps"
+  fixes a:: "'a ::{field, ring_char_0} fps"
   assumes
       ra0: "r k (a $ 0) ^ k = a $ 0"
   and rb0: "r k (b $ 0) ^ k = b $ 0"
@@ -1818,7 +1816,7 @@
 subsection{* Compositional inverses *}
 
 
-fun compinv :: "'a fps \<Rightarrow> nat \<Rightarrow> 'a::{recpower,field}" where
+fun compinv :: "'a fps \<Rightarrow> nat \<Rightarrow> 'a::{field}" where
   "compinv a 0 = X$0"
 | "compinv a (Suc n) = (X$ Suc n - setsum (\<lambda>i. (compinv a i) * (a^i)$Suc n) {0 .. n}) / (a$1) ^ Suc n"
 
@@ -1849,7 +1847,7 @@
 qed
 
 
-fun gcompinv :: "'a fps \<Rightarrow> 'a fps \<Rightarrow> nat \<Rightarrow> 'a::{recpower,field}" where
+fun gcompinv :: "'a fps \<Rightarrow> 'a fps \<Rightarrow> nat \<Rightarrow> 'a::{field}" where
   "gcompinv b a 0 = b$0"
 | "gcompinv b a (Suc n) = (b$ Suc n - setsum (\<lambda>i. (gcompinv b a i) * (a^i)$Suc n) {0 .. n}) / (a$1) ^ Suc n"
 
@@ -2102,7 +2100,7 @@
 qed
 
 lemma fps_inv_deriv:
-  assumes a0:"a$0 = (0::'a::{recpower,field})" and a1: "a$1 \<noteq> 0"
+  assumes a0:"a$0 = (0::'a::{field})" and a1: "a$1 \<noteq> 0"
   shows "fps_deriv (fps_inv a) = inverse (fps_deriv a oo fps_inv a)"
 proof-
   let ?ia = "fps_inv a"
@@ -2122,7 +2120,7 @@
 subsubsection{* Exponential series *}
 definition "E x = Abs_fps (\<lambda>n. x^n / of_nat (fact n))"
 
-lemma E_deriv[simp]: "fps_deriv (E a) = fps_const (a::'a::{field, recpower, ring_char_0}) * E a" (is "?l = ?r")
+lemma E_deriv[simp]: "fps_deriv (E a) = fps_const (a::'a::{field, ring_char_0}) * E a" (is "?l = ?r")
 proof-
   {fix n
     have "?l$n = ?r $ n"
@@ -2132,7 +2130,7 @@
 qed
 
 lemma E_unique_ODE:
-  "fps_deriv a = fps_const c * a \<longleftrightarrow> a = fps_const (a$0) * E (c :: 'a::{field, ring_char_0, recpower})"
+  "fps_deriv a = fps_const c * a \<longleftrightarrow> a = fps_const (a$0) * E (c :: 'a::{field, ring_char_0})"
   (is "?lhs \<longleftrightarrow> ?rhs")
 proof-
   {assume d: ?lhs
@@ -2159,7 +2157,7 @@
 ultimately show ?thesis by blast
 qed
 
-lemma E_add_mult: "E (a + b) = E (a::'a::{ring_char_0, field, recpower}) * E b" (is "?l = ?r")
+lemma E_add_mult: "E (a + b) = E (a::'a::{ring_char_0, field}) * E b" (is "?l = ?r")
 proof-
   have "fps_deriv (?r) = fps_const (a+b) * ?r"
     by (simp add: fps_const_add[symmetric] ring_simps del: fps_const_add)
@@ -2171,10 +2169,10 @@
 lemma E_nth[simp]: "E a $ n = a^n / of_nat (fact n)"
   by (simp add: E_def)
 
-lemma E0[simp]: "E (0::'a::{field, recpower}) = 1"
+lemma E0[simp]: "E (0::'a::{field}) = 1"
   by (simp add: fps_eq_iff power_0_left)
 
-lemma E_neg: "E (- a) = inverse (E (a::'a::{ring_char_0, field, recpower}))"
+lemma E_neg: "E (- a) = inverse (E (a::'a::{ring_char_0, field}))"
 proof-
   from E_add_mult[of a "- a"] have th0: "E a * E (- a) = 1"
     by (simp )
@@ -2182,7 +2180,7 @@
   from fps_inverse_unique[OF th1 th0] show ?thesis by simp
 qed
 
-lemma E_nth_deriv[simp]: "fps_nth_deriv n (E (a::'a::{field, recpower, ring_char_0})) = (fps_const a)^n * (E a)"
+lemma E_nth_deriv[simp]: "fps_nth_deriv n (E (a::'a::{field, ring_char_0})) = (fps_const a)^n * (E a)"
   by (induct n, auto simp add: power_Suc)
 
 lemma fps_compose_uminus: "- (a::'a::ring_1 fps) oo c = - (a oo c)"
@@ -2195,7 +2193,7 @@
 lemma X_fps_compose:"X oo a = Abs_fps (\<lambda>n. if n = 0 then (0::'a::comm_ring_1) else a$n)"
   by (simp add: fps_eq_iff fps_compose_nth mult_delta_left setsum_delta power_Suc)
 
-lemma X_compose_E[simp]: "X oo E (a::'a::{field, recpower}) = E a - 1"
+lemma X_compose_E[simp]: "X oo E (a::'a::{field}) = E a - 1"
   by (simp add: fps_eq_iff X_fps_compose)
 
 lemma LE_compose:
@@ -2217,7 +2215,7 @@
 
 
 lemma inverse_one_plus_X:
-  "inverse (1 + X) = Abs_fps (\<lambda>n. (- 1 ::'a::{field, recpower})^n)"
+  "inverse (1 + X) = Abs_fps (\<lambda>n. (- 1 ::'a::{field})^n)"
   (is "inverse ?l = ?r")
 proof-
   have th: "?l * ?r = 1"
@@ -2228,11 +2226,11 @@
   from fps_inverse_unique[OF th' th] show ?thesis .
 qed
 
-lemma E_power_mult: "(E (c::'a::{field,recpower,ring_char_0}))^n = E (of_nat n * c)"
+lemma E_power_mult: "(E (c::'a::{field,ring_char_0}))^n = E (of_nat n * c)"
   by (induct n, auto simp add: ring_simps E_add_mult power_Suc)
 
 subsubsection{* Logarithmic series *}
-definition "(L::'a::{field, ring_char_0,recpower} fps)
+definition "(L::'a::{field, ring_char_0} fps)
   = Abs_fps (\<lambda>n. (- 1) ^ Suc n / of_nat n)"
 
 lemma fps_deriv_L: "fps_deriv L = inverse (1 + X)"
@@ -2243,7 +2241,7 @@
   by (simp add: L_def)
 
 lemma L_E_inv:
-  assumes a: "a\<noteq> (0::'a::{field,division_by_zero,ring_char_0,recpower})"
+  assumes a: "a\<noteq> (0::'a::{field,division_by_zero,ring_char_0})"
   shows "L = fps_const a * fps_inv (E a - 1)" (is "?l = ?r")
 proof-
   let ?b = "E a - 1"
@@ -2267,10 +2265,10 @@
 
 subsubsection{* Formal trigonometric functions  *}
 
-definition "fps_sin (c::'a::{field, recpower, ring_char_0}) =
+definition "fps_sin (c::'a::{field, ring_char_0}) =
   Abs_fps (\<lambda>n. if even n then 0 else (- 1) ^((n - 1) div 2) * c^n /(of_nat (fact n)))"
 
-definition "fps_cos (c::'a::{field, recpower, ring_char_0}) = Abs_fps (\<lambda>n. if even n then (- 1) ^ (n div 2) * c^n / (of_nat (fact n)) else 0)"
+definition "fps_cos (c::'a::{field, ring_char_0}) = Abs_fps (\<lambda>n. if even n then (- 1) ^ (n div 2) * c^n / (of_nat (fact n)) else 0)"
 
 lemma fps_sin_deriv:
   "fps_deriv (fps_sin c) = fps_const c * fps_cos c"
diff -r 9999a77590c3 -r 53642251a04f src/HOL/Library/FrechetDeriv.thy
--- a/src/HOL/Library/FrechetDeriv.thy	Tue Apr 28 19:15:50 2009 +0200
+++ b/src/HOL/Library/FrechetDeriv.thy	Wed Apr 29 14:20:26 2009 +0200
@@ -382,7 +382,7 @@
 subsection {* Powers *}
 
 lemma FDERIV_power_Suc:
-  fixes x :: "'a::{real_normed_algebra,recpower,comm_ring_1}"
+  fixes x :: "'a::{real_normed_algebra,comm_ring_1}"
   shows "FDERIV (\<lambda>x. x ^ Suc n) x :> (\<lambda>h. (1 + of_nat n) * x ^ n * h)"
  apply (induct n)
   apply (simp add: power_Suc FDERIV_ident)
@@ -392,7 +392,7 @@
 done
 
 lemma FDERIV_power:
-  fixes x :: "'a::{real_normed_algebra,recpower,comm_ring_1}"
+  fixes x :: "'a::{real_normed_algebra,comm_ring_1}"
   shows "FDERIV (\<lambda>x. x ^ n) x :> (\<lambda>h. of_nat n * x ^ (n - 1) * h)"
   apply (cases n)
    apply (simp add: FDERIV_const)
diff -r 9999a77590c3 -r 53642251a04f src/HOL/Library/Fundamental_Theorem_Algebra.thy
--- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Tue Apr 28 19:15:50 2009 +0200
+++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Wed Apr 29 14:20:26 2009 +0200
@@ -560,14 +560,14 @@
   done
 
 lemma poly_replicate_append:
-  "poly (monom 1 n * p) (x::'a::{recpower, comm_ring_1}) = x^n * poly p x"
+  "poly (monom 1 n * p) (x::'a::{comm_ring_1}) = x^n * poly p x"
   by (simp add: poly_monom)
 
 text {* Decomposition of polynomial, skipping zero coefficients
   after the first.  *}
 
 lemma poly_decompose_lemma:
- assumes nz: "\<not>(\<forall>z. z\<noteq>0 \<longrightarrow> poly p z = (0::'a::{recpower,idom}))"
+ assumes nz: "\<not>(\<forall>z. z\<noteq>0 \<longrightarrow> poly p z = (0::'a::{idom}))"
   shows "\<exists>k a q. a\<noteq>0 \<and> Suc (psize q + k) = psize p \<and>
                  (\<forall>z. poly p z = z^k * poly (pCons a q) z)"
 unfolding psize_def
@@ -595,7 +595,7 @@
 
 lemma poly_decompose:
   assumes nc: "~constant(poly p)"
-  shows "\<exists>k a q. a\<noteq>(0::'a::{recpower,idom}) \<and> k\<noteq>0 \<and>
+  shows "\<exists>k a q. a\<noteq>(0::'a::{idom}) \<and> k\<noteq>0 \<and>
                psize q + k + 1 = psize p \<and>
               (\<forall>z. poly p z = poly p 0 + z^k * poly (pCons a q) z)"
 using nc
diff -r 9999a77590c3 -r 53642251a04f src/HOL/Library/Numeral_Type.thy
--- a/src/HOL/Library/Numeral_Type.thy	Tue Apr 28 19:15:50 2009 +0200
+++ b/src/HOL/Library/Numeral_Type.thy	Wed Apr 29 14:20:26 2009 +0200
@@ -216,12 +216,6 @@
 apply (simp_all add: Rep_simps zmod_simps ring_simps)
 done
 
-lemma recpower: "OFCLASS('a, recpower_class)"
-apply (intro_classes, unfold definitions)
-apply (simp_all add: Rep_simps zmod_simps add_ac mult_assoc
-                     mod_pos_pos_trivial size1)
-done
-
 end
 
 locale mod_ring = mod_type +
@@ -340,11 +334,11 @@
 apply (rule uminus_bit1_def [unfolded Abs_bit1'_def])
 done
 
-instance bit0 :: (finite) "{comm_ring_1,recpower}"
-  by (rule bit0.comm_ring_1 bit0.recpower)+
+instance bit0 :: (finite) comm_ring_1
+  by (rule bit0.comm_ring_1)+
 
-instance bit1 :: (finite) "{comm_ring_1,recpower}"
-  by (rule bit1.comm_ring_1 bit1.recpower)+
+instance bit1 :: (finite) comm_ring_1
+  by (rule bit1.comm_ring_1)+
 
 instantiation bit0 and bit1 :: (finite) number_ring
 begin
diff -r 9999a77590c3 -r 53642251a04f src/HOL/Library/Pocklington.thy
--- a/src/HOL/Library/Pocklington.thy	Tue Apr 28 19:15:50 2009 +0200
+++ b/src/HOL/Library/Pocklington.thy	Wed Apr 29 14:20:26 2009 +0200
@@ -568,7 +568,7 @@
 
 lemma nproduct_cmul:
   assumes fS:"finite S"
-  shows "setprod (\<lambda>m. (c::'a::{comm_monoid_mult,recpower})* a(m)) S = c ^ (card S) * setprod a S"
+  shows "setprod (\<lambda>m. (c::'a::{comm_monoid_mult})* a(m)) S = c ^ (card S) * setprod a S"
 unfolding setprod_timesf setprod_constant[OF fS, of c] ..
 
 lemma coprime_nproduct:
diff -r 9999a77590c3 -r 53642251a04f src/HOL/Library/Polynomial.thy
--- a/src/HOL/Library/Polynomial.thy	Tue Apr 28 19:15:50 2009 +0200
+++ b/src/HOL/Library/Polynomial.thy	Wed Apr 29 14:20:26 2009 +0200
@@ -632,8 +632,6 @@
   shows "a \<noteq> 0 \<Longrightarrow> p dvd smult a q \<longleftrightarrow> p dvd q"
   by (safe elim!: dvd_smult dvd_smult_cancel)
 
-instance poly :: (comm_semiring_1) recpower ..
-
 lemma degree_power_le: "degree (p ^ n) \<le> degree p * n"
 by (induct n, simp, auto intro: order_trans degree_mult_le)
 
@@ -1120,7 +1118,7 @@
   unfolding one_poly_def by simp
 
 lemma poly_monom:
-  fixes a x :: "'a::{comm_semiring_1,recpower}"
+  fixes a x :: "'a::{comm_semiring_1}"
   shows "poly (monom a n) x = a * x ^ n"
   by (induct n, simp add: monom_0, simp add: monom_Suc power_Suc mult_ac)
 
@@ -1149,7 +1147,7 @@
   by (induct p, simp_all, simp add: algebra_simps)
 
 lemma poly_power [simp]:
-  fixes p :: "'a::{comm_semiring_1,recpower} poly"
+  fixes p :: "'a::{comm_semiring_1} poly"
   shows "poly (p ^ n) x = poly p x ^ n"
   by (induct n, simp, simp add: power_Suc)
 
diff -r 9999a77590c3 -r 53642251a04f src/HOL/Library/Univ_Poly.thy
--- a/src/HOL/Library/Univ_Poly.thy	Tue Apr 28 19:15:50 2009 +0200
+++ b/src/HOL/Library/Univ_Poly.thy	Wed Apr 29 14:20:26 2009 +0200
@@ -167,22 +167,9 @@
     simp_all add: poly_cmult poly_add left_distrib right_distrib mult_ac)
 qed
 
-class recpower_semiring = semiring + recpower
-class recpower_semiring_1 = semiring_1 + recpower
-class recpower_semiring_0 = semiring_0 + recpower
-class recpower_ring = ring + recpower
-class recpower_ring_1 = ring_1 + recpower
-subclass (in recpower_ring_1) recpower_ring ..
-class recpower_comm_semiring_1 = recpower + comm_semiring_1
-class recpower_comm_ring_1 = recpower + comm_ring_1
-subclass (in recpower_comm_ring_1) recpower_comm_semiring_1 ..
-class recpower_idom = recpower + idom
-subclass (in recpower_idom) recpower_comm_ring_1 ..
 class idom_char_0 = idom + ring_char_0
-class recpower_idom_char_0 = recpower + idom_char_0
-subclass (in recpower_idom_char_0) recpower_idom ..
 
-lemma (in recpower_comm_ring_1) poly_exp: "poly (p %^ n) x = (poly p x) ^ n"
+lemma (in comm_ring_1) poly_exp: "poly (p %^ n) x = (poly p x) ^ n"
 apply (induct "n")
 apply (auto simp add: poly_cmult poly_mult power_Suc)
 done
@@ -418,7 +405,7 @@
   finally show ?thesis .
 qed
 
-lemma (in recpower_idom) poly_exp_eq_zero[simp]:
+lemma (in idom) poly_exp_eq_zero[simp]:
      "(poly (p %^ n) = poly []) = (poly p = poly [] & n \<noteq> 0)"
 apply (simp only: fun_eq add: all_simps [symmetric])
 apply (rule arg_cong [where f = All])
@@ -437,7 +424,7 @@
 apply simp
 done
 
-lemma (in recpower_idom) poly_exp_prime_eq_zero: "(poly ([a, 1] %^ n) \<noteq> poly [])"
+lemma (in idom) poly_exp_prime_eq_zero: "(poly ([a, 1] %^ n) \<noteq> poly [])"
 by auto
 
 text{*A more constructive notion of polynomials being trivial*}
@@ -507,7 +494,7 @@
 done
 
 
-lemma (in recpower_comm_semiring_1) poly_divides_exp: "m \<le> n ==> (p %^ m) divides (p %^ n)"
+lemma (in comm_semiring_1) poly_divides_exp: "m \<le> n ==> (p %^ m) divides (p %^ n)"
 apply (auto simp add: le_iff_add)
 apply (induct_tac k)
 apply (rule_tac [2] poly_divides_trans)
@@ -516,7 +503,7 @@
 apply (auto simp add: poly_mult fun_eq mult_ac)
 done
 
-lemma (in recpower_comm_semiring_1) poly_exp_divides: "[| (p %^ n) divides q;  m\<le>n |] ==> (p %^ m) divides q"
+lemma (in comm_semiring_1) poly_exp_divides: "[| (p %^ n) divides q;  m\<le>n |] ==> (p %^ m) divides q"
 by (blast intro: poly_divides_exp poly_divides_trans)
 
 lemma (in comm_semiring_0) poly_divides_add:
@@ -583,7 +570,7 @@
 qed
 
 
-lemma (in recpower_comm_semiring_1) poly_mulexp: "poly (mulexp n p q) x = (poly p x) ^ n * poly q x"
+lemma (in comm_semiring_1) poly_mulexp: "poly (mulexp n p q) x = (poly p x) ^ n * poly q x"
 by(induct n, auto simp add: poly_mult power_Suc mult_ac)
 
 lemma (in comm_semiring_1) divides_left_mult:
@@ -600,11 +587,11 @@
 
 (* FIXME: Tidy up *)
 
-lemma (in recpower_semiring_1)
+lemma (in semiring_1)
   zero_power_iff: "0 ^ n = (if n = 0 then 1 else 0)"
   by (induct n, simp_all add: power_Suc)
 
-lemma (in recpower_idom_char_0) poly_order_exists:
+lemma (in idom_char_0) poly_order_exists:
   assumes lp: "length p = d" and p0: "poly p \<noteq> poly []"
   shows "\<exists>n. ([-a, 1] %^ n) divides p & ~(([-a, 1] %^ (Suc n)) divides p)"
 proof-
@@ -637,7 +624,7 @@
 lemma (in semiring_1) poly_one_divides[simp]: "[1] divides p"
 by (simp add: divides_def, auto)
 
-lemma (in recpower_idom_char_0) poly_order: "poly p \<noteq> poly []
+lemma (in idom_char_0) poly_order: "poly p \<noteq> poly []
       ==> EX! n. ([-a, 1] %^ n) divides p &
                  ~(([-a, 1] %^ (Suc n)) divides p)"
 apply (auto intro: poly_order_exists simp add: less_linear simp del: pmult_Cons pexp_Suc)
@@ -652,7 +639,7 @@
 lemma some1_equalityD: "[| n = (@n. P n); EX! n. P n |] ==> P n"
 by (blast intro: someI2)
 
-lemma (in recpower_idom_char_0) order:
+lemma (in idom_char_0) order:
       "(([-a, 1] %^ n) divides p &
         ~(([-a, 1] %^ (Suc n)) divides p)) =
         ((n = order a p) & ~(poly p = poly []))"
@@ -662,17 +649,17 @@
 apply (blast intro!: poly_order [THEN [2] some1_equalityD])
 done
 
-lemma (in recpower_idom_char_0) order2: "[| poly p \<noteq> poly [] |]
+lemma (in idom_char_0) order2: "[| poly p \<noteq> poly [] |]
       ==> ([-a, 1] %^ (order a p)) divides p &
               ~(([-a, 1] %^ (Suc(order a p))) divides p)"
 by (simp add: order del: pexp_Suc)
 
-lemma (in recpower_idom_char_0) order_unique: "[| poly p \<noteq> poly []; ([-a, 1] %^ n) divides p;
+lemma (in idom_char_0) order_unique: "[| poly p \<noteq> poly []; ([-a, 1] %^ n) divides p;
          ~(([-a, 1] %^ (Suc n)) divides p)
       |] ==> (n = order a p)"
 by (insert order [of a n p], auto)
 
-lemma (in recpower_idom_char_0) order_unique_lemma: "(poly p \<noteq> poly [] & ([-a, 1] %^ n) divides p &
+lemma (in idom_char_0) order_unique_lemma: "(poly p \<noteq> poly [] & ([-a, 1] %^ n) divides p &
          ~(([-a, 1] %^ (Suc n)) divides p))
       ==> (n = order a p)"
 by (blast intro: order_unique)
@@ -692,7 +679,7 @@
 apply (auto simp add: divides_def poly_mult simp del: pmult_Cons)
 done
 
-lemma (in recpower_idom_char_0) order_root: "(poly p a = 0) = ((poly p = poly []) | order a p \<noteq> 0)"
+lemma (in idom_char_0) order_root: "(poly p a = 0) = ((poly p = poly []) | order a p \<noteq> 0)"
 proof-
   let ?poly = poly
   show ?thesis
@@ -706,7 +693,7 @@
 done
 qed
 
-lemma (in recpower_idom_char_0) order_divides: "(([-a, 1] %^ n) divides p) = ((poly p = poly []) | n \<le> order a p)"
+lemma (in idom_char_0) order_divides: "(([-a, 1] %^ n) divides p) = ((poly p = poly []) | n \<le> order a p)"
 proof-
   let ?poly = poly
   show ?thesis
@@ -718,7 +705,7 @@
 done
 qed
 
-lemma (in recpower_idom_char_0) order_decomp:
+lemma (in idom_char_0) order_decomp:
      "poly p \<noteq> poly []
       ==> \<exists>q. (poly p = poly (([-a, 1] %^ (order a p)) *** q)) &
                 ~([-a, 1] divides q)"
@@ -732,7 +719,7 @@
 
 text{*Important composition properties of orders.*}
 lemma order_mult: "poly (p *** q) \<noteq> poly []
-      ==> order a (p *** q) = order a p + order (a::'a::{recpower_idom_char_0}) q"
+      ==> order a (p *** q) = order a p + order (a::'a::{idom_char_0}) q"
 apply (cut_tac a = a and p = "p *** q" and n = "order a p + order a q" in order)
 apply (auto simp add: poly_entire simp del: pmult_Cons)
 apply (drule_tac a = a in order2)+
@@ -753,7 +740,7 @@
 apply (simp add: fun_eq poly_exp_add poly_mult mult_ac del: pmult_Cons)
 done
 
-lemma (in recpower_idom_char_0) order_mult:
+lemma (in idom_char_0) order_mult:
   assumes pq0: "poly (p *** q) \<noteq> poly []"
   shows "order a (p *** q) = order a p + order a q"
 proof-
@@ -783,7 +770,7 @@
 done
 qed
 
-lemma (in recpower_idom_char_0) order_root2: "poly p \<noteq> poly [] ==> (poly p a = 0) = (order a p \<noteq> 0)"
+lemma (in idom_char_0) order_root2: "poly p \<noteq> poly [] ==> (poly p a = 0) = (order a p \<noteq> 0)"
 by (rule order_root [THEN ssubst], auto)
 
 lemma (in semiring_1) pmult_one[simp]: "[1] *** p = p" by auto
@@ -791,7 +778,7 @@
 lemma (in semiring_0) poly_Nil_zero: "poly [] = poly [0]"
 by (simp add: fun_eq)
 
-lemma (in recpower_idom_char_0) rsquarefree_decomp:
+lemma (in idom_char_0) rsquarefree_decomp:
      "[| rsquarefree p; poly p a = 0 |]
       ==> \<exists>q. (poly p = poly ([-a, 1] *** q)) & poly q a \<noteq> 0"
 apply (simp add: rsquarefree_def, safe)
@@ -999,7 +986,7 @@
   ultimately show ?case by blast
 qed
 
-lemma (in recpower_idom_char_0) order_degree:
+lemma (in idom_char_0) order_degree:
   assumes p0: "poly p \<noteq> poly []"
   shows "order a p \<le> degree p"
 proof-
diff -r 9999a77590c3 -r 53642251a04f src/HOL/Library/comm_ring.ML
--- a/src/HOL/Library/comm_ring.ML	Tue Apr 28 19:15:50 2009 +0200
+++ b/src/HOL/Library/comm_ring.ML	Wed Apr 29 14:20:26 2009 +0200
@@ -65,7 +65,7 @@
   | reif_polex T vs t = polex_pol T $ reif_pol T vs t;
 
 (* reification of the equation *)
-val TFree (_, cr_sort) = @{typ "'a :: {comm_ring, recpower}"};
+val cr_sort = @{sort "comm_ring_1"};
 
 fun reif_eq thy (eq as Const("op =", Type("fun", [T, _])) $ lhs $ rhs) =
       if Sign.of_sort thy (T, cr_sort) then
diff -r 9999a77590c3 -r 53642251a04f src/HOL/NSA/StarDef.thy
--- a/src/HOL/NSA/StarDef.thy	Tue Apr 28 19:15:50 2009 +0200
+++ b/src/HOL/NSA/StarDef.thy	Wed Apr 29 14:20:26 2009 +0200
@@ -954,8 +954,6 @@
 
 subsection {* Power *}
 
-instance star :: (recpower) recpower ..
-
 lemma star_power_def [transfer_unfold]:
   "(op ^) \<equiv> \<lambda>x n. ( *f* (\<lambda>x. x ^ n)) x"
 proof (rule eq_reflection, rule ext, rule ext)
diff -r 9999a77590c3 -r 53642251a04f src/HOL/Power.thy
--- a/src/HOL/Power.thy	Tue Apr 28 19:15:50 2009 +0200
+++ b/src/HOL/Power.thy	Wed Apr 29 14:20:26 2009 +0200
@@ -419,13 +419,9 @@
 apply assumption
 done
 
-class recpower = monoid_mult
-
 
 subsection {* Exponentiation for the Natural Numbers *}
 
-instance nat :: recpower ..
-
 lemma nat_one_le_power [simp]:
   "Suc 0 \<le> i \<Longrightarrow> Suc 0 \<le> i ^ n"
   by (rule one_le_power [of i n, unfolded One_nat_def])
diff -r 9999a77590c3 -r 53642251a04f src/HOL/Rational.thy
--- a/src/HOL/Rational.thy	Tue Apr 28 19:15:50 2009 +0200
+++ b/src/HOL/Rational.thy	Wed Apr 29 14:20:26 2009 +0200
@@ -834,8 +834,6 @@
   "q \<in> \<rat> \<Longrightarrow> (\<And>r. P (of_rat r)) \<Longrightarrow> P q"
   by (rule Rats_cases) auto
 
-instance rat :: recpower ..
-
 
 subsection {* Implementation of rational numbers as pairs of integers *}
 
diff -r 9999a77590c3 -r 53642251a04f src/HOL/RealPow.thy
--- a/src/HOL/RealPow.thy	Tue Apr 28 19:15:50 2009 +0200
+++ b/src/HOL/RealPow.thy	Wed Apr 29 14:20:26 2009 +0200
@@ -12,8 +12,6 @@
 
 declare abs_mult_self [simp]
 
-instance real :: recpower ..
-
 lemma two_realpow_ge_one [simp]: "(1::real) \<le> 2 ^ n"
 by simp
 
diff -r 9999a77590c3 -r 53642251a04f src/HOL/SizeChange/Graphs.thy
--- a/src/HOL/SizeChange/Graphs.thy	Tue Apr 28 19:15:50 2009 +0200
+++ b/src/HOL/SizeChange/Graphs.thy	Wed Apr 29 14:20:26 2009 +0200
@@ -228,7 +228,7 @@
   qed
 qed
 
-instance graph :: (type, monoid_mult) "{semiring_1, idem_add, recpower}"
+instance graph :: (type, monoid_mult) "{semiring_1, idem_add}"
 proof
   fix a b c :: "('a, 'b) graph"
   
diff -r 9999a77590c3 -r 53642251a04f src/HOL/SizeChange/Kleene_Algebras.thy
--- a/src/HOL/SizeChange/Kleene_Algebras.thy	Tue Apr 28 19:15:50 2009 +0200
+++ b/src/HOL/SizeChange/Kleene_Algebras.thy	Wed Apr 29 14:20:26 2009 +0200
@@ -97,7 +97,7 @@
   and star4: "x * a \<le> x \<Longrightarrow> x * star a \<le> x"
 
 class kleene_by_complete_lattice = pre_kleene
-  + complete_lattice + recpower + star +
+  + complete_lattice + power + star +
   assumes star_cont: "a * star b * c = SUPR UNIV (\<lambda>n. a * b ^ n * c)"
 begin
 
diff -r 9999a77590c3 -r 53642251a04f src/HOL/Word/WordArith.thy
--- a/src/HOL/Word/WordArith.thy	Tue Apr 28 19:15:50 2009 +0200
+++ b/src/HOL/Word/WordArith.thy	Wed Apr 29 14:20:26 2009 +0200
@@ -778,8 +778,6 @@
   apply (simp add: word_mult_1)
   done
 
-instance word :: (len0) recpower ..
-
 instance word :: (len0) comm_semiring 
   by (intro_classes) (simp add : word_left_distrib)
 
@@ -790,8 +788,6 @@
 instance word :: (len) comm_semiring_1 
   by (intro_classes) (simp add: lenw1_zero_neq_one)
 
-instance word :: (len) recpower ..
-
 instance word :: (len) comm_ring_1 ..
 
 instance word :: (len0) comm_semiring_0 ..
diff -r 9999a77590c3 -r 53642251a04f src/HOL/ex/Commutative_Ring_Complete.thy
--- a/src/HOL/ex/Commutative_Ring_Complete.thy	Tue Apr 28 19:15:50 2009 +0200
+++ b/src/HOL/ex/Commutative_Ring_Complete.thy	Wed Apr 29 14:20:26 2009 +0200
@@ -1,5 +1,4 @@
-(*  ID:         $Id$
-    Author:     Bernhard Haeupler
+(*  Author:     Bernhard Haeupler
 
 This theory is about of the relative completeness of method comm-ring
 method.  As long as the reified atomic polynomials of type 'a pol are
@@ -14,7 +13,7 @@
 
 text {* Formalization of normal form *}
 fun
-  isnorm :: "('a::{comm_ring,recpower}) pol \<Rightarrow> bool"
+  isnorm :: "('a::{comm_ring}) pol \<Rightarrow> bool"
 where
     "isnorm (Pc c) \<longleftrightarrow> True"
   | "isnorm (Pinj i (Pc c)) \<longleftrightarrow> False"
diff -r 9999a77590c3 -r 53642251a04f src/HOL/ex/Formal_Power_Series_Examples.thy
--- a/src/HOL/ex/Formal_Power_Series_Examples.thy	Tue Apr 28 19:15:50 2009 +0200
+++ b/src/HOL/ex/Formal_Power_Series_Examples.thy	Wed Apr 29 14:20:26 2009 +0200
@@ -11,7 +11,7 @@
 
 section{* The generalized binomial theorem *}
 lemma gbinomial_theorem: 
-  "((a::'a::{ring_char_0, field, division_by_zero, recpower})+b) ^ n = (\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(n-k))"
+  "((a::'a::{ring_char_0, field, division_by_zero})+b) ^ n = (\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(n-k))"
 proof-
   from E_add_mult[of a b] 
   have "(E (a + b)) $ n = (E a * E b)$n" by simp
@@ -38,7 +38,7 @@
   by (simp add: fps_binomial_def)
 
 lemma fps_binomial_ODE_unique:
-  fixes c :: "'a::{field, recpower,ring_char_0}"
+  fixes c :: "'a::{field, ring_char_0}"
   shows "fps_deriv a = (fps_const c * a) / (1 + X) \<longleftrightarrow> a = fps_const (a$0) * fps_binomial c"
   (is "?lhs \<longleftrightarrow> ?rhs")
 proof-
diff -r 9999a77590c3 -r 53642251a04f src/HOL/ex/Groebner_Examples.thy
--- 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)
diff -r 9999a77590c3 -r 53642251a04f src/HOL/ex/Numeral.thy
--- a/src/HOL/ex/Numeral.thy	Tue Apr 28 19:15:50 2009 +0200
+++ b/src/HOL/ex/Numeral.thy	Wed Apr 29 14:20:26 2009 +0200
@@ -14,25 +14,19 @@
 
 text {* Increment function for type @{typ num} *}
 
-primrec
-  inc :: "num \<Rightarrow> num"
-where
+primrec inc :: "num \<Rightarrow> num" where
   "inc One = Dig0 One"
 | "inc (Dig0 x) = Dig1 x"
 | "inc (Dig1 x) = Dig0 (inc x)"
 
 text {* Converting between type @{typ num} and type @{typ nat} *}
 
-primrec
-  nat_of_num :: "num \<Rightarrow> nat"
-where
+primrec nat_of_num :: "num \<Rightarrow> nat" where
   "nat_of_num One = Suc 0"
 | "nat_of_num (Dig0 x) = nat_of_num x + nat_of_num x"
 | "nat_of_num (Dig1 x) = Suc (nat_of_num x + nat_of_num x)"
 
-primrec
-  num_of_nat :: "nat \<Rightarrow> num"
-where
+primrec num_of_nat :: "nat \<Rightarrow> num" where
   "num_of_nat 0 = One"
 | "num_of_nat (Suc n) = (if 0 < n then inc (num_of_nat n) else One)"
 
@@ -719,32 +713,32 @@
    (simp_all add: of_num.simps of_num_plus [symmetric] algebra_simps)
 
 lemma of_num_pow:
-  "(of_num (pow x y)::'a::{semiring_numeral,recpower}) = of_num x ^ of_num y"
+  "(of_num (pow x y)::'a::{semiring_numeral}) = of_num x ^ of_num y"
 by (induct y)
    (simp_all add: of_num.simps of_num_square of_num_times [symmetric]
                   power_Suc power_add)
 
 lemma power_of_num [numeral]:
-  "of_num x ^ of_num y = (of_num (pow x y)::'a::{semiring_numeral,recpower})"
+  "of_num x ^ of_num y = (of_num (pow x y)::'a::{semiring_numeral})"
   by (rule of_num_pow [symmetric])
 
 lemma power_zero_of_num [numeral]:
-  "0 ^ of_num n = (0::'a::{semiring_0,recpower})"
+  "0 ^ of_num n = (0::'a::{semiring_0,power})"
   using of_num_pos [where n=n and ?'a=nat]
   by (simp add: power_0_left)
 
 lemma power_minus_one_double:
-  "(- 1) ^ (n + n) = (1::'a::{ring_1,recpower})"
+  "(- 1) ^ (n + n) = (1::'a::{ring_1})"
   by (induct n) (simp_all add: power_Suc)
 
 lemma power_minus_Dig0 [numeral]:
-  fixes x :: "'a::{ring_1,recpower}"
+  fixes x :: "'a::{ring_1}"
   shows "(- x) ^ of_num (Dig0 n) = x ^ of_num (Dig0 n)"
   by (subst power_minus)
      (simp add: of_num.simps power_minus_one_double)
 
 lemma power_minus_Dig1 [numeral]:
-  fixes x :: "'a::{ring_1,recpower}"
+  fixes x :: "'a::{ring_1}"
   shows "(- x) ^ of_num (Dig1 n) = - (x ^ of_num (Dig1 n))"
   by (subst power_minus)
      (simp add: of_num.simps power_Suc power_minus_one_double)
diff -r 9999a77590c3 -r 53642251a04f src/HOL/ex/ReflectionEx.thy
--- a/src/HOL/ex/ReflectionEx.thy	Tue Apr 28 19:15:50 2009 +0200
+++ b/src/HOL/ex/ReflectionEx.thy	Wed Apr 29 14:20:26 2009 +0200
@@ -385,7 +385,7 @@
   (* An example for equations containing type variables *)	
 datatype prod = Zero | One | Var nat | Mul prod prod 
   | Pw prod nat | PNM nat nat prod
-consts Iprod :: " prod \<Rightarrow> ('a::{ordered_idom,recpower}) list \<Rightarrow>'a" 
+consts Iprod :: " prod \<Rightarrow> ('a::{ordered_idom}) list \<Rightarrow>'a" 
 primrec
   "Iprod Zero vs = 0"
   "Iprod One vs = 1"
@@ -397,7 +397,7 @@
 datatype sgn = Pos prod | Neg prod | ZeroEq prod | NZeroEq prod | Tr | F 
   | Or sgn sgn | And sgn sgn
 
-consts Isgn :: " sgn \<Rightarrow> ('a::{ordered_idom, recpower}) list \<Rightarrow>bool"
+consts Isgn :: " sgn \<Rightarrow> ('a::{ordered_idom}) list \<Rightarrow>bool"
 primrec 
   "Isgn Tr vs = True"
   "Isgn F vs = False"
@@ -410,7 +410,7 @@
 
 lemmas eqs = Isgn.simps Iprod.simps
 
-lemma "(x::'a::{ordered_idom, recpower})^4 * y * z * y^2 * z^23 > 0"
+lemma "(x::'a::{ordered_idom})^4 * y * z * y^2 * z^23 > 0"
   apply (reify eqs)
   oops