NEWS
changeset 68404 05605481935d
parent 68393 b9989df11c78
parent 68403 223172b97d0b
child 68450 41de07c7a0f3
     1.1 --- a/NEWS	Wed Jun 06 17:18:48 2018 +0200
     1.2 +++ b/NEWS	Wed Jun 06 18:20:03 2018 +0200
     1.3 @@ -202,6 +202,12 @@
     1.4  locale instances where the qualifier's sole purpose is avoiding
     1.5  duplicate constant declarations.
     1.6  
     1.7 +* Proof method 'simp' now supports a new modifier 'flip:' followed by a list
     1.8 +of theorems. Each of these theorems is removed from the simpset
     1.9 +(without warning if it is not there) and the symmetric version of the theorem
    1.10 +(i.e. lhs and rhs exchanged) is added to the simpset.
    1.11 +For 'auto' and friends the modifier is "simp flip:".
    1.12 +
    1.13  
    1.14  *** Pure ***
    1.15