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. Userlevel 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 