| changeset 60429 | d3d1e185cd63 |
| parent 60352 | d46de31a50c4 |
| child 60500 | 903bb1495239 |
--- a/src/HOL/Library/Extended_Real.thy Thu Jun 11 21:41:55 2015 +0100 +++ b/src/HOL/Library/Extended_Real.thy Fri Jun 12 08:53:23 2015 +0200 @@ -1403,7 +1403,7 @@ by (auto intro: ereal_cases) termination by (relation "{}") simp -definition "divide x y = x * inverse (y :: ereal)" +definition "x div y = x * inverse (y :: ereal)" instance ..