NEWS
changeset 68260 61188c781cdd
parent 68249 949d93804740
child 68276 cbee43ff4ceb
     1.1 --- a/NEWS	Thu May 24 07:59:41 2018 +0200
     1.2 +++ b/NEWS	Thu May 24 09:18:29 2018 +0200
     1.3 @@ -347,6 +347,11 @@
     1.4  
     1.5  INCOMPATIBILITY.
     1.6  
     1.7 +* Classical setup: Assumption "m mod d = 0" (for m d :: nat) is no
     1.8 +longer aggresively destroyed to "?q. m = d * q".  INCOMPATIBILITY,
     1.9 +adding "elim!: dvd" to classical proof methods in most situations
    1.10 +restores broken proofs.
    1.11 +
    1.12  
    1.13  *** ML ***
    1.14