--- a/NEWS Wed Jun 06 13:04:52 2018 +0200
+++ b/NEWS Wed Jun 06 18:19:55 2018 +0200
@@ -195,6 +195,12 @@
locale instances where the qualifier's sole purpose is avoiding
duplicate constant declarations.
+* Proof method 'simp' now supports a new modifier 'flip:' followed by a list
+of theorems. Each of these theorems is removed from the simpset
+(without warning if it is not there) and the symmetric version of the theorem
+(i.e. lhs and rhs exchanged) is added to the simpset.
+For 'auto' and friends the modifier is "simp flip:".
+
*** Pure ***