# HG changeset patch
# User huffman
# Date 1316618933 25200
# Node ID ad016fc215f2487fc56f839d2c7cc766ee701d75
# Parent  34e5fc15ea0231bc08e8ee0dd83f67f4b7061543
remove redundant instantiation ereal :: power

diff -r 34e5fc15ea02 -r ad016fc215f2 src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Wed Sep 21 06:41:34 2011 -0700
+++ b/src/HOL/Library/Extended_Real.thy	Wed Sep 21 08:28:53 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)