src/HOL/Complex.thy
changeset 31021 53642251a04f
parent 30960 fec1a04b7220
child 31292 d24b2692562f
--- 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