# HG changeset patch
# User krauss
# Date 1269983575 -7200
# Node ID 10563d88c0b6ae07a8ceebacca3b83b72079f254
# Parent  d149c3886e7e9002b5240ffb6fe1e84cf5ceb6c5
NEWS

diff -r d149c3886e7e -r 10563d88c0b6 NEWS
--- 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 ***