src/HOL/Complex.thy
changeset 36409 d323e7773aa8
parent 36349 39be26d1bc28
child 36777 be5461582d0f
     1.1 --- a/src/HOL/Complex.thy	Mon Apr 26 11:34:19 2010 +0200
     1.2 +++ b/src/HOL/Complex.thy	Mon Apr 26 15:37:50 2010 +0200
     1.3 @@ -99,7 +99,7 @@
     1.4  
     1.5  subsection {* Multiplication and Division *}
     1.6  
     1.7 -instantiation complex :: "{field, division_ring_inverse_zero}"
     1.8 +instantiation complex :: field_inverse_zero
     1.9  begin
    1.10  
    1.11  definition