diff -r 04deeb14327c -r d72ca5742f80 NEWS --- a/NEWS Wed Aug 22 21:43:17 2012 +0200 +++ b/NEWS Wed Aug 22 22:47:16 2012 +0200 @@ -6,6 +6,9 @@ *** General *** +* Command 'ML_file' evaluates ML text from a file directly within the +theory, without any predeclaration via 'uses' in the theory header. + * Discontinued obsolete method fastsimp / tactic fast_simp_tac, which is called fastforce / fast_force_tac already since Isabelle2011-1.