--- a/NEWS Sat May 28 17:35:12 2016 +0200
+++ b/NEWS Sat May 28 21:38:58 2016 +0200
@@ -70,6 +70,10 @@
eigen-context, e.g. 'axiomatization', 'definition', 'inductive',
'function'.
+* Command 'axiomatization' has become more restrictive to correspond
+better to internal axioms as singleton facts with mandatory name. Minor
+INCOMPATIBILITY.
+
* Toplevel theorem statements support eigen-context notation with 'if' /
'for' (in postix), which corresponds to 'assumes' / 'fixes' in the
traditional long statement form (in prefix). Local premises are called