NEWS
changeset 51313 102a0a0718c5
parent 51295 71fc3776c453
child 51316 dfe469293eb4
--- a/NEWS	Thu Feb 28 16:19:08 2013 +0100
+++ b/NEWS	Thu Feb 28 16:38:17 2013 +0100
@@ -14,6 +14,13 @@
 'ML_file' in Isabelle2013.  Minor INCOMPATIBILITY.
 
 
+*** Pure ***
+
+* Discontinued obsolete 'axioms' command, which has been marked as
+legacy since Isabelle2009-2.  INCOMPATIBILITY, use 'axiomatization'
+instead, while observing its uniform scope for polymorphism.
+
+
 *** HOL ***
 
 * Discontinued obsolete src/HOL/IsaMakefile (considered legacy since