src/HOL/Complex.thy
changeset 31021 53642251a04f
parent 30960 fec1a04b7220
child 31292 d24b2692562f
     1.1 --- a/src/HOL/Complex.thy	Tue Apr 28 19:15:50 2009 +0200
     1.2 +++ b/src/HOL/Complex.thy	Wed Apr 29 14:20:26 2009 +0200
     1.3 @@ -157,11 +157,6 @@
     1.4  end
     1.5  
     1.6  
     1.7 -subsection {* Exponentiation *}
     1.8 -
     1.9 -instance complex :: recpower ..
    1.10 -
    1.11 -
    1.12  subsection {* Numerals and Arithmetic *}
    1.13  
    1.14  instantiation complex :: number_ring