| changeset 51295 | 71fc3776c453 |
| parent 51293 | 05b1bbae748d |
| child 51313 | 102a0a0718c5 |
--- a/NEWS Wed Feb 27 16:27:44 2013 +0100 +++ b/NEWS Wed Feb 27 17:32:17 2013 +0100 @@ -10,6 +10,9 @@ commands like 'ML_file' work without separate declaration of file dependencies. Minor INCOMPATIBILITY. +* Discontinued redundant 'use' command, which was superseded by +'ML_file' in Isabelle2013. Minor INCOMPATIBILITY. + *** HOL ***