1.1 --- a/src/HOL/Real/RealPow.thy	Thu Nov 27 10:47:55 2003 +0100
     1.2 +++ b/src/HOL/Real/RealPow.thy	Fri Nov 28 12:09:37 2003 +0100
     1.3 @@ -6,10 +6,7 @@
     1.4  
     1.5  *)
     1.6  
     1.7 -theory RealPow = RealAbs:
     1.8 -
     1.9 -(*belongs to theory RealAbs*)
    1.10 -lemmas [arith_split] = abs_split
    1.11 +theory RealPow = RealArith:
    1.12  
    1.13  instance real :: power ..
    1.14