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