equal
deleted
inserted
replaced
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 |
141 |
142 * Proof terms: Type substitutions on proof constants now use canonical |
142 * Proof terms: Type substitutions on proof constants now use canonical |
143 order of type variables. Potential INCOMPATIBILITY for tools working |
143 order of type variables. INCOMPATIBILITY for tools working with proof |
144 with proof terms. |
144 terms. |
145 |
145 |
146 * New operation Thm.unconstrainT eliminates all sort constraints from |
146 * New operation Thm.unconstrainT eliminates all sort constraints from |
147 a theorem and proof, introducing explicit OFCLASS-premises. On the |
147 a theorem and proof, introducing explicit OFCLASS-premises. On the |
148 proof term level, this operation is automatically applied at PThm |
148 proof term level, this operation is automatically applied at PThm |
149 boundaries, such that closed proofs are always free of sort |
149 boundaries, such that closed proofs are always free of sort |