--- a/src/HOL/Real/RealPow.thy Thu Nov 01 21:12:13 2001 +0100
+++ b/src/HOL/Real/RealPow.thy Fri Nov 02 17:55:24 2001 +0100
@@ -15,7 +15,7 @@
instance real :: power ..
primrec (realpow)
- realpow_0: "r ^ 0 = Numeral1"
+ realpow_0: "r ^ 0 = 1"
realpow_Suc: "r ^ (Suc n) = (r::real) * (r ^ n)"
end