--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Real/RealPow.thy	Fri Jul 23 17:29:12 1999 +0200
@@ -0,0 +1,16 @@
+(*  Title       : RealPow.thy
+    Author      : Jacques D. Fleuriot  
+    Copyright   : 1998  University of Cambridge
+    Description : Natural powers theory
+
+*)
+
+RealPow = WF_Rel + RealAbs + 
+
+instance real :: {power}
+
+primrec
+     realpow_0   "r ^ 0       = 1r"
+     realpow_Suc "r ^ (Suc n) = (r::real) * (r ^ n)"
+
+end