equal
deleted
inserted
replaced
3 |
3 |
4 New in this Isabelle version |
4 New in this Isabelle version |
5 ---------------------------- |
5 ---------------------------- |
6 |
6 |
7 *** General *** |
7 *** General *** |
|
8 |
|
9 * Command 'ML_file' evaluates ML text from a file directly within the |
|
10 theory, without any predeclaration via 'uses' in the theory header. |
8 |
11 |
9 * Discontinued obsolete method fastsimp / tactic fast_simp_tac, which |
12 * Discontinued obsolete method fastsimp / tactic fast_simp_tac, which |
10 is called fastforce / fast_force_tac already since Isabelle2011-1. |
13 is called fastforce / fast_force_tac already since Isabelle2011-1. |
11 |
14 |
12 * Updated and extended "isar-ref" manual, reduced remaining material |
15 * Updated and extended "isar-ref" manual, reduced remaining material |