NEWS
changeset 68403 223172b97d0b
parent 68373 f254e383bfe9
child 68404 05605481935d
     1.1 --- a/NEWS	Wed Jun 06 13:04:52 2018 +0200
     1.2 +++ b/NEWS	Wed Jun 06 18:19:55 2018 +0200
     1.3 @@ -195,6 +195,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