# HG changeset patch
# User krauss
# Date 1275575945 -7200
# Node ID 12790d670662d7af583062019afe3024fcdbf5e5
# Parent  812ff0bbd6773762c49ffc01540faf9b41ac6cb6
mention unconstrain in NEWS

diff -r 812ff0bbd677 -r 12790d670662 NEWS
--- a/NEWS	Wed Jun 02 22:45:50 2010 +0200
+++ b/NEWS	Thu Jun 03 16:39:05 2010 +0200
@@ -143,6 +143,13 @@
 order of type variables. Potential INCOMPATIBILITY for tools working
 with proof terms.
 
+* New operation Thm.unconstrainT eliminates all sort constraints from
+a theorem and proof, introducing explicit OFCLASS-premises. On the
+proof term level, this operation is automatically applied at PThm
+boundaries, such that closed proofs are always free of sort
+constraints. The old (axiomatic) unconstrain operation has been
+discontinued.  INCOMPATIBILITY for tools working with proof terms.
+
 
 *** HOL ***