diff -r ad1ffcc90162 -r e96d5c42c4b0 src/HOL/Complex/ComplexBin.thy
--- a/src/HOL/Complex/ComplexBin.thy	Sat Feb 14 02:06:12 2004 +0100
+++ b/src/HOL/Complex/ComplexBin.thy	Sun Feb 15 10:46:37 2004 +0100
@@ -5,18 +5,5 @@
                 This case is reduced to that for the reals.
 *)
 
-ComplexBin = Complex + 
-
-
-instance
-  complex :: number 
-
-instance complex :: plus_ac0(complex_add_commute,complex_add_assoc,complex_add_zero_left)
+theory ComplexBin = Complex:
 
-
-defs
-  complex_number_of_def
-    "number_of v == complex_of_real (number_of v)"
-     (*::bin=>complex               ::bin=>complex*)
-
-end