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])