| changeset 36044 | 10563d88c0b6 |
| parent 36000 | 5560b2437789 |
| child 36096 | abc6a2ea4b88 |
--- a/NEWS Tue Mar 30 15:25:35 2010 +0200 +++ b/NEWS Tue Mar 30 23:12:55 2010 +0200 @@ -96,6 +96,10 @@ without introducing dependencies on parameters or assumptions, which is not possible in Isabelle/Pure. +* Proof terms: Type substitutions on proof constants now use canonical +order of type variables. INCOMPATIBILITY: Tools working with proof +terms may need to be adapted. + *** HOL ***