--- 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 ***