diff -r 9999a77590c3 -r 53642251a04f src/HOL/Complex.thy --- a/src/HOL/Complex.thy Tue Apr 28 19:15:50 2009 +0200 +++ b/src/HOL/Complex.thy Wed Apr 29 14:20:26 2009 +0200 @@ -157,11 +157,6 @@ end -subsection {* Exponentiation *} - -instance complex :: recpower .. - - subsection {* Numerals and Arithmetic *} instantiation complex :: number_ring