# HG changeset patch
# User krauss
# Date 1275660166 -7200
# Node ID 52dc576f1759a07693d5b22a829ba471880958b1
# Parent  664d3110beb2da56e8ca6b34f03f56e738bd6436
NEWS (more strict internal axioms/defs format)

diff -r 664d3110beb2 -r 52dc576f1759 NEWS
--- a/NEWS	Fri Jun 04 11:31:33 2010 +0200
+++ b/NEWS	Fri Jun 04 16:02:46 2010 +0200
@@ -139,6 +139,10 @@
 * Command 'defaultsort' has been renamed to 'default_sort', it works
 within a local theory context.  Minor INCOMPATIBILITY.
 
+* Raw axioms/defs may no longer carry sort constraints, and raw defs
+may no longer carry premises. User-level specifications are
+transformed accordingly by Thm.add_axiom/add_def.
+
 * Proof terms: Type substitutions on proof constants now use canonical
 order of type variables.  INCOMPATIBILITY for tools working with proof
 terms.