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