--- 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