# HG changeset patch
# User wenzelm
# Date 964476219 -7200
# Node ID c3a13a7d442435d3f1a81150e070558588c66111
# Parent  d2fa043ab24f49efa1abb067f5a97456e3f31979
lemmas [arith_split] = abs_split (*belongs to theory RealAbs*);

diff -r d2fa043ab24f -r c3a13a7d4424 src/HOL/Real/RealPow.thy
--- 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