# HG changeset patch
# User haftmann
# Date 1207575452 -7200
# Node ID 522f45a8604e8f70be7741e79f28e370957a8304
# Parent  631ce7f6bdc6223fd87be64addcb2421d6e246d7
instantiation replacing primitive instance plus overloaded defs; realpow.simps now named power_real.simps

diff -r 631ce7f6bdc6 -r 522f45a8604e src/HOL/Real/RealPow.thy
--- a/src/HOL/Real/RealPow.thy	Mon Apr 07 15:37:31 2008 +0200
+++ b/src/HOL/Real/RealPow.thy	Mon Apr 07 15:37:32 2008 +0200
@@ -12,21 +12,22 @@
 
 declare abs_mult_self [simp]
 
-instance real :: power ..
+instantiation real :: recpower
+begin
 
-primrec (realpow)
-     realpow_0:   "r ^ 0       = 1"
-     realpow_Suc: "r ^ (Suc n) = (r::real) * (r ^ n)"
+primrec power_real where
+  realpow_0:     "r ^ 0     = (1\<Colon>real)"
+  | realpow_Suc: "r ^ Suc n = (r\<Colon>real) * r ^ n"
 
-
-instance real :: recpower
-proof
+instance proof
   fix z :: real
   fix n :: nat
   show "z^0 = 1" by simp
   show "z^(Suc n) = z * (z^n)" by simp
 qed
 
+end
+
 
 lemma two_realpow_ge_one [simp]: "(1::real) \<le> 2 ^ n"
 by simp