src/HOL/Library/Extended_Real.thy
changeset 45036 ad016fc215f2
parent 44928 7ef6505bde7f
child 45236 ac4a2a66707d
     1.1 --- a/src/HOL/Library/Extended_Real.thy	Wed Sep 21 06:41:34 2011 -0700
     1.2 +++ b/src/HOL/Library/Extended_Real.thy	Wed Sep 21 08:28:53 2011 -0700
     1.3 @@ -765,14 +765,6 @@
     1.4  
     1.5  subsubsection {* Power *}
     1.6  
     1.7 -instantiation ereal :: power
     1.8 -begin
     1.9 -primrec power_ereal where
    1.10 -  "power_ereal x 0 = 1" |
    1.11 -  "power_ereal x (Suc n) = x * x ^ n"
    1.12 -instance ..
    1.13 -end
    1.14 -
    1.15  lemma ereal_power[simp]: "(ereal x) ^ n = ereal (x^n)"
    1.16    by (induct n) (auto simp: one_ereal_def)
    1.17