changeset 48890 | d72ca5742f80 |
parent 48844 | 6408fb6f7d81 |
child 48936 | e6d9e46ff7bc |
--- 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.