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