src/HOL/Complex.thy
changeset 30960 fec1a04b7220
parent 30729 461ee3e49ad3
child 31021 53642251a04f
     1.1 --- a/src/HOL/Complex.thy	Wed Apr 22 19:09:19 2009 +0200
     1.2 +++ b/src/HOL/Complex.thy	Wed Apr 22 19:09:21 2009 +0200
     1.3 @@ -159,19 +159,7 @@
     1.4  
     1.5  subsection {* Exponentiation *}
     1.6  
     1.7 -instantiation complex :: recpower
     1.8 -begin
     1.9 -
    1.10 -primrec power_complex where
    1.11 -  "z ^ 0     = (1\<Colon>complex)"
    1.12 -| "z ^ Suc n = (z\<Colon>complex) * z ^ n"
    1.13 -
    1.14 -instance proof
    1.15 -qed simp_all
    1.16 -
    1.17 -declare power_complex.simps [simp del]
    1.18 -
    1.19 -end
    1.20 +instance complex :: recpower ..
    1.21  
    1.22  
    1.23  subsection {* Numerals and Arithmetic *}