NEWS
changeset 60352 d46de31a50c4
parent 60347 7d64ad9910e2
child 60370 9ec1d3d2068e
     1.1 --- a/NEWS	Mon Jun 01 18:59:21 2015 +0200
     1.2 +++ b/NEWS	Mon Jun 01 18:59:21 2015 +0200
     1.3 @@ -36,6 +36,14 @@
     1.4  * Nitpick:
     1.5    - Removed "check_potential" and "check_genuine" options.
     1.6  
     1.7 +* Constants Fields.divide (... / ...) and Divides.div (... div ...)
     1.8 +are logically unified to Rings.divide in syntactic type class
     1.9 +Rings.divide, with particular infix syntax added as abbreviations
    1.10 +in classes Fields.inverse and Divides.div respectively.  INCOMPATIBILITY,
    1.11 +instantiatios must refer to Rings.divide rather than the former
    1.12 +separate constants, and infix syntax is usually not available during
    1.13 +instantiation.
    1.14 +
    1.15  
    1.16  New in Isabelle2015 (May 2015)
    1.17  ------------------------------