--- a/src/HOL/Real/RealPow.thy Thu Nov 27 10:47:55 2003 +0100
+++ b/src/HOL/Real/RealPow.thy Fri Nov 28 12:09:37 2003 +0100
@@ -6,10 +6,7 @@
*)
-theory RealPow = RealAbs:
-
-(*belongs to theory RealAbs*)
-lemmas [arith_split] = abs_split
+theory RealPow = RealArith:
instance real :: power ..