NEWS
changeset 68404 05605481935d
parent 68393 b9989df11c78
parent 68403 223172b97d0b
child 68450 41de07c7a0f3
--- a/NEWS	Wed Jun 06 17:18:48 2018 +0200
+++ b/NEWS	Wed Jun 06 18:20:03 2018 +0200
@@ -202,6 +202,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 ***