# HG changeset patch
# User wenzelm
# Date 1224189908 -7200
# Node ID c5a915b453906f61108cb139001019662712a810
# Parent  06737d425249a42af41af24ae62d5323af30d963
goal-directed proof now enforces strict proof irrelevance wrt. sort hypotheses;

diff -r 06737d425249 -r c5a915b45390 NEWS
--- a/NEWS	Thu Oct 16 22:44:37 2008 +0200
+++ b/NEWS	Thu Oct 16 22:45:08 2008 +0200
@@ -47,6 +47,19 @@
 
 *** Pure ***
 
+* Goal-directed proof now enforces strict proof irrelevance wrt. sort
+hypotheses.  Sorts required in the course of reasoning need to be
+covered by the constraints in the initial statement, completed by the
+type instance information of the background theory.  Non-trivial sort
+hypotheses, which rarely occur in practice, may be specified via
+vacuous propositions of the form SORT_CONSTRAIN('a::c).  For example:
+
+  lemma assumes "SORT_CONSTRAINT('a::empty)" shows False ...
+
+The result contains an implicit sort hypotheses as before --
+SORT_CONSTRAINT premises are is eliminated as part of the canonical
+rule normalization.
+
 * Changed defaults for unify configuration options:
 
   unify_trace_bound = 50 (formerly 25)