lemmas [arith_split] = abs_split (*belongs to theory RealAbs*);

--- a/src/HOL/Real/RealPow.thy	Tue Jul 25 00:02:52 2000 +0200
+++ b/src/HOL/Real/RealPow.thy	Tue Jul 25 00:03:39 2000 +0200
@@ -1,4 +1,4 @@
-(*  Title       : RealPow.thy
+(*  Title       : HOL/Real/RealPow.thy
     ID          : $Id$
     Author      : Jacques D. Fleuriot  
     Copyright   : 1998  University of Cambridge
@@ -6,12 +6,17 @@
 
 *)
 
-RealPow = RealAbs +
+theory RealPow = RealAbs:
 
-instance real :: {power}
+(*belongs to theory RealAbs*)
+lemmas [arith_split] = abs_split
+
+
+instance real :: power
+  by intro_classes
 
 primrec (realpow)
-     realpow_0   "r ^ 0       = #1"
-     realpow_Suc "r ^ (Suc n) = (r::real) * (r ^ n)"
+     realpow_0:   "r ^ 0       = #1"
+     realpow_Suc: "r ^ (Suc n) = (r::real) * (r ^ n)"
 
 end