--- a/src/HOL/Power.thy Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Power.thy Mon Aug 16 14:22:27 2004 +0200
@@ -7,7 +7,9 @@
header{*Exponentiation and Binomial Coefficients*}
-theory Power = Divides:
+theory Power
+import Divides
+begin
subsection{*Powers for Arbitrary Semirings*}