NEWS
changeset 48890 d72ca5742f80
parent 48844 6408fb6f7d81
child 48936 e6d9e46ff7bc
     1.1 --- a/NEWS	Wed Aug 22 21:43:17 2012 +0200
     1.2 +++ b/NEWS	Wed Aug 22 22:47:16 2012 +0200
     1.3 @@ -6,6 +6,9 @@
     1.4  
     1.5  *** General ***
     1.6  
     1.7 +* Command 'ML_file' evaluates ML text from a file directly within the
     1.8 +theory, without any predeclaration via 'uses' in the theory header.
     1.9 +
    1.10  * Discontinued obsolete method fastsimp / tactic fast_simp_tac, which
    1.11  is called fastforce / fast_force_tac already since Isabelle2011-1.
    1.12