NEWS
changeset 49243 ded41f584938
parent 49190 e1e1d427747d
child 49310 6e30078de4f0
     1.1 --- a/NEWS	Mon Sep 10 12:00:28 2012 +0200
     1.2 +++ b/NEWS	Mon Sep 10 12:13:39 2012 +0200
     1.3 @@ -9,6 +9,12 @@
     1.4  * Command 'ML_file' evaluates ML text from a file directly within the
     1.5  theory, without any predeclaration via 'uses' in the theory header.
     1.6  
     1.7 +* Old command 'use' command and corresponding keyword 'uses' in the
     1.8 +theory header are legacy features and will be discontinued soon.
     1.9 +Tools that load their additional source files may imitate the
    1.10 +'ML_file' implementation, such that the system can take care of
    1.11 +dependencies properly.
    1.12 +
    1.13  * Discontinued obsolete method fastsimp / tactic fast_simp_tac, which
    1.14  is called fastforce / fast_force_tac already since Isabelle2011-1.
    1.15