src/HOL/Real/RealPow.thy
changeset 12018 ec054019c910
parent 11701 3d51fbf81c17
child 14265 95b42e69436c
     1.1 --- a/src/HOL/Real/RealPow.thy	Thu Nov 01 21:12:13 2001 +0100
     1.2 +++ b/src/HOL/Real/RealPow.thy	Fri Nov 02 17:55:24 2001 +0100
     1.3 @@ -15,7 +15,7 @@
     1.4  instance real :: power ..
     1.5  
     1.6  primrec (realpow)
     1.7 -     realpow_0:   "r ^ 0       = Numeral1"
     1.8 +     realpow_0:   "r ^ 0       = 1"
     1.9       realpow_Suc: "r ^ (Suc n) = (r::real) * (r ^ n)"
    1.10  
    1.11  end