src/HOL/Real/RealPow.thy
changeset 8856 435187ffc64e
parent 7219 4e3f386c2e37
child 9013 9dd0274f76af
     1.1 --- a/src/HOL/Real/RealPow.thy	Wed May 10 21:04:16 2000 +0200
     1.2 +++ b/src/HOL/Real/RealPow.thy	Wed May 10 22:34:30 2000 +0200
     1.3 @@ -6,11 +6,11 @@
     1.4  
     1.5  *)
     1.6  
     1.7 -RealPow = WF_Rel + RealAbs + 
     1.8 +RealPow = RealAbs +
     1.9  
    1.10  instance real :: {power}
    1.11  
    1.12 -primrec
    1.13 +primrec (realpow)
    1.14       realpow_0   "r ^ 0       = 1r"
    1.15       realpow_Suc "r ^ (Suc n) = (r::real) * (r ^ n)"
    1.16