equal
deleted
inserted
replaced
192 |
192 |
193 * For rewrites clauses, if activating a locale instance fails, fall |
193 * For rewrites clauses, if activating a locale instance fails, fall |
194 back to reading the clause first. This helps avoid qualification of |
194 back to reading the clause first. This helps avoid qualification of |
195 locale instances where the qualifier's sole purpose is avoiding |
195 locale instances where the qualifier's sole purpose is avoiding |
196 duplicate constant declarations. |
196 duplicate constant declarations. |
|
197 |
|
198 * Proof method 'simp' now supports a new modifier 'flip:' followed by a list |
|
199 of theorems. Each of these theorems is removed from the simpset |
|
200 (without warning if it is not there) and the symmetric version of the theorem |
|
201 (i.e. lhs and rhs exchanged) is added to the simpset. |
|
202 For 'auto' and friends the modifier is "simp flip:". |
197 |
203 |
198 |
204 |
199 *** Pure *** |
205 *** Pure *** |
200 |
206 |
201 * The inner syntax category "sort" now includes notation "_" for the |
207 * The inner syntax category "sort" now includes notation "_" for the |