# 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.