equal
deleted
inserted
replaced
136 context -- without introducing dependencies on parameters or |
136 context -- without introducing dependencies on parameters or |
137 assumptions, which is not possible in Isabelle/Pure. |
137 assumptions, which is not possible in Isabelle/Pure. |
138 |
138 |
139 * Command 'defaultsort' has been renamed to 'default_sort', it works |
139 * Command 'defaultsort' has been renamed to 'default_sort', it works |
140 within a local theory context. Minor INCOMPATIBILITY. |
140 within a local theory context. Minor INCOMPATIBILITY. |
|
141 |
|
142 * Raw axioms/defs may no longer carry sort constraints, and raw defs |
|
143 may no longer carry premises. User-level specifications are |
|
144 transformed accordingly by Thm.add_axiom/add_def. |
141 |
145 |
142 * Proof terms: Type substitutions on proof constants now use canonical |
146 * Proof terms: Type substitutions on proof constants now use canonical |
143 order of type variables. INCOMPATIBILITY for tools working with proof |
147 order of type variables. INCOMPATIBILITY for tools working with proof |
144 terms. |
148 terms. |
145 |
149 |