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 |
|
179 *** Pure *** |
|
180 |
|
181 * The inner syntax category "sort" now includes notation "_" for the |
|
182 dummy sort: it is effectively ignored in type-inference. |
177 |
183 |
178 |
184 |
179 *** HOL *** |
185 *** HOL *** |
180 |
186 |
181 * Clarifed theorem names: |
187 * Clarifed theorem names: |