# HG changeset patch
# User huffman
# Date 1316627995 25200
# Node ID 29b5ff81f709a79f4049f539f4ff00cb02da9036
# Parent  ad016fc215f2487fc56f839d2c7cc766ee701d75# Parent  60d2c03d5c70cfac2d6fa691c46d0f47cf88031a
merged

diff -r 60d2c03d5c70 -r 29b5ff81f709 src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Wed Sep 21 15:55:16 2011 +0200
+++ b/src/HOL/Library/Extended_Real.thy	Wed Sep 21 10:59:55 2011 -0700
@@ -765,14 +765,6 @@
 
 subsubsection {* Power *}
 
-instantiation ereal :: power
-begin
-primrec power_ereal where
-  "power_ereal x 0 = 1" |
-  "power_ereal x (Suc n) = x * x ^ n"
-instance ..
-end
-
 lemma ereal_power[simp]: "(ereal x) ^ n = ereal (x^n)"
   by (induct n) (auto simp: one_ereal_def)