174 improves modularity of proofs and scalability of locale interpretation. |
174 improves modularity of proofs and scalability of locale interpretation. |
175 Rare INCOMPATIBILITY, need to refer to explicitly named facts instead |
175 Rare INCOMPATIBILITY, need to refer to explicitly named facts instead |
176 (e.g. use 'find_theorems' or 'try' to figure this out). |
176 (e.g. use 'find_theorems' or 'try' to figure this out). |
177 |
177 |
178 * Rewrites clauses (keyword 'rewrites') were moved into the locale |
178 * Rewrites clauses (keyword 'rewrites') were moved into the locale |
179 expression syntax, where they are part of locale instances. Keyword |
179 expression syntax, where they are part of locale instances. In |
180 'for' now needs to occur after, not before 'rewrites'. |
180 interpretation commands rewrites clauses now need to occur before |
181 Minor INCOMPATIBILITY. |
181 'for' and 'defines'. Minor INCOMPATIBILITY. |
182 |
182 |
183 * For rewrites clauses in locale expressions, if activating a locale |
183 * For rewrites clauses, if activating a locale instance fails, fall |
184 instance fails, fall back to reading the clause first. This helps |
184 back to reading the clause first. This helps avoid qualification of |
185 avoiding qualified locale instances where the qualifier's sole purpose |
185 locale instances where the qualifier's sole purpose is avoiding |
186 is avoiding duplicate constant declarations. |
186 duplicate constant declarations. |
187 |
187 |
188 |
188 |
189 *** Pure *** |
189 *** Pure *** |
190 |
190 |
191 * The inner syntax category "sort" now includes notation "_" for the |
191 * The inner syntax category "sort" now includes notation "_" for the |