| changeset 60352 | d46de31a50c4 |
| parent 60017 | b785d6d06430 |
| child 60429 | d3d1e185cd63 |
--- a/src/HOL/Complex.thy Mon Jun 01 18:59:21 2015 +0200 +++ b/src/HOL/Complex.thy Mon Jun 01 18:59:21 2015 +0200 @@ -70,7 +70,7 @@ "Re (inverse x) = Re x / ((Re x)\<^sup>2 + (Im x)\<^sup>2)" | "Im (inverse x) = - Im x / ((Re x)\<^sup>2 + (Im x)\<^sup>2)" -definition "x / (y\<Colon>complex) = x * inverse y" +definition "divide x (y\<Colon>complex) = x * inverse y" instance by intro_classes