| changeset 60429 | d3d1e185cd63 |
| parent 60352 | d46de31a50c4 |
| child 60758 | d8d85a8172b5 |
--- a/src/HOL/Complex.thy Thu Jun 11 21:41:55 2015 +0100 +++ b/src/HOL/Complex.thy Fri Jun 12 08:53:23 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 "divide x (y\<Colon>complex) = x * inverse y" +definition "x div (y\<Colon>complex) = x * inverse y" instance by intro_classes