equal
deleted
inserted
replaced
9 * Discontinued obsolete method fastsimp / tactic fast_simp_tac, which |
9 * Discontinued obsolete method fastsimp / tactic fast_simp_tac, which |
10 is called fastforce / fast_force_tac already since Isabelle2011-1. |
10 is called fastforce / fast_force_tac already since Isabelle2011-1. |
11 |
11 |
12 * Updated and extended "isar-ref" manual, reduced remaining material |
12 * Updated and extended "isar-ref" manual, reduced remaining material |
13 in old "ref" manual. |
13 in old "ref" manual. |
|
14 |
|
15 |
|
16 *** Pure *** |
|
17 |
|
18 * Discontinued obsolete attribute "COMP". Potential INCOMPATIBILITY, |
|
19 use regular rule composition via "OF" / "THEN", or explicit proof |
|
20 structure instead. Note that Isabelle/ML provides a variety of |
|
21 operators like COMP, INCR_COMP, COMP_INCR, which need to be applied |
|
22 with some care where this is really required. |
14 |
23 |
15 |
24 |
16 *** Document preparation *** |
25 *** Document preparation *** |
17 |
26 |
18 * Default for \<euro> is now based on eurosym package, instead of |
27 * Default for \<euro> is now based on eurosym package, instead of |