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