equal
deleted
inserted
replaced
172 * Command 'interpret' no longer exposes resulting theorems as literal |
172 * Command 'interpret' no longer exposes resulting theorems as literal |
173 facts, notably for the \<open>prop\<close> notation or the "fact" proof method. This |
173 facts, notably for the \<open>prop\<close> notation or the "fact" proof method. This |
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 |
|
178 * Rewrites clauses (keyword 'rewrites') were moved into the locale |
|
179 expression syntax, where they are part of locale instances. Keyword |
|
180 'for' now needs to occur after, not before 'rewrites'. |
|
181 Minor INCOMPATIBILITY. |
177 |
182 |
178 |
183 |
179 *** Pure *** |
184 *** Pure *** |
180 |
185 |
181 * The inner syntax category "sort" now includes notation "_" for the |
186 * The inner syntax category "sort" now includes notation "_" for the |