equal
deleted
inserted
replaced
99 |
99 |
100 * Commands 'type_notation' and 'no_type_notation' declare type syntax |
100 * Commands 'type_notation' and 'no_type_notation' declare type syntax |
101 within a local theory context, with explicit checking of the |
101 within a local theory context, with explicit checking of the |
102 constructors involved (in contrast to the raw 'syntax' versions). |
102 constructors involved (in contrast to the raw 'syntax' versions). |
103 |
103 |
104 * Command 'typedecl' now works within a local theory context -- |
104 * Commands 'types' and 'typedecl' now work within a local theory |
105 without introducing dependencies on parameters or assumptions, which |
105 context -- without introducing dependencies on parameters or |
106 is not possible in Isabelle/Pure. |
106 assumptions, which is not possible in Isabelle/Pure. |
107 |
107 |
108 * Proof terms: Type substitutions on proof constants now use canonical |
108 * Proof terms: Type substitutions on proof constants now use canonical |
109 order of type variables. INCOMPATIBILITY: Tools working with proof |
109 order of type variables. INCOMPATIBILITY: Tools working with proof |
110 terms may need to be adapted. |
110 terms may need to be adapted. |
111 |
111 |