# HG changeset patch
# User huffman
# Date 1180464793 -7200
# Node ID 892e0a4551da3e5b82e8c5e0f45bbc06f8df3e64
# Parent  e2e370bccde1050e2920ad231a2152f6833085b2
use new-style instance declarations

diff -r e2e370bccde1 -r 892e0a4551da src/HOL/Complex/Complex.thy
--- a/src/HOL/Complex/Complex.thy	Tue May 29 20:31:53 2007 +0200
+++ b/src/HOL/Complex/Complex.thy	Tue May 29 20:53:13 2007 +0200
@@ -13,10 +13,10 @@
 
 datatype complex = Complex real real
 
-instance complex :: "{zero, one, plus, times, minus, inverse, power}" ..
-
-consts
+definition
   "ii"    :: complex    ("\<i>")
+where
+  i_def: "ii == Complex 0 1"
 
 consts Re :: "complex => real"
 primrec Re: "Re (Complex x y) = x"
@@ -27,32 +27,32 @@
 lemma complex_surj [simp]: "Complex (Re z) (Im z) = z"
   by (induct z) simp
 
-defs (overloaded)
-
+instance complex :: zero
   complex_zero_def:
-  "0 == Complex 0 0"
+  "0 == Complex 0 0" ..
 
+instance complex :: one
   complex_one_def:
-  "1 == Complex 1 0"
+  "1 == Complex 1 0" ..
+
+instance complex :: plus
+  complex_add_def:
+    "z + w == Complex (Re z + Re w) (Im z + Im w)" ..
 
-  i_def: "ii == Complex 0 1"
+instance complex :: minus
+  complex_minus_def: "- z == Complex (- Re z) (- Im z)"
+  complex_diff_def:
+    "z - w == z + - (w::complex)" ..
 
-  complex_minus_def: "- z == Complex (- Re z) (- Im z)"
+instance complex :: times
+  complex_mult_def:
+    "z * w == Complex (Re z * Re w - Im z * Im w) (Re z * Im w + Im z * Re w)" ..
 
+instance complex :: inverse
   complex_inverse_def:
    "inverse z ==
     Complex (Re z / ((Re z)\<twosuperior> + (Im z)\<twosuperior>)) (- Im z / ((Re z)\<twosuperior> + (Im z)\<twosuperior>))"
-
-  complex_add_def:
-    "z + w == Complex (Re z + Re w) (Im z + Im w)"
-
-  complex_diff_def:
-    "z - w == z + - (w::complex)"
-
-  complex_mult_def:
-    "z * w == Complex (Re z * Re w - Im z * Im w) (Re z * Im w + Im z * Re w)"
-
-  complex_divide_def: "w / (z::complex) == w * inverse z"
+  complex_divide_def: "w / (z::complex) == w * inverse z" ..
 
 
 lemma complex_equality [intro?]: "Re z = Re w ==> Im z = Im w ==> z = w"
@@ -500,6 +500,8 @@
 
 subsection{*Exponentiation*}
 
+instance complex :: power ..
+
 primrec
      complexpow_0:   "z ^ 0       = 1"
      complexpow_Suc: "z ^ (Suc n) = (z::complex) * (z ^ n)"