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