equal
deleted
inserted
replaced
7 *** General *** |
7 *** General *** |
8 |
8 |
9 * Prover IDE (PIDE) improvements: |
9 * Prover IDE (PIDE) improvements: |
10 . parallel terminal proofs ('by'); |
10 . parallel terminal proofs ('by'); |
11 . improved output panel with tooltips, hyperlinks etc.; |
11 . improved output panel with tooltips, hyperlinks etc.; |
|
12 . improved tooltips with nested tooltips, hyperlinks etc.; |
12 . more efficient painting, improved reactivity; |
13 . more efficient painting, improved reactivity; |
13 . more robust incremental parsing of outer syntax (partial |
14 . more robust incremental parsing of outer syntax (partial |
14 comments, malformed symbols); |
15 comments, malformed symbols); |
15 . smarter handling of tracing messages (via tracing_limit); |
16 . smarter handling of tracing messages (via tracing_limit); |
16 . more plugin options and preferences, based on Isabelle/Scala; |
17 . more plugin options and preferences, based on Isabelle/Scala; |
33 * Discontinued obsolete method fastsimp / tactic fast_simp_tac, which |
34 * Discontinued obsolete method fastsimp / tactic fast_simp_tac, which |
34 is called fastforce / fast_force_tac already since Isabelle2011-1. |
35 is called fastforce / fast_force_tac already since Isabelle2011-1. |
35 |
36 |
36 * Updated and extended "isar-ref" manual, reduced remaining material |
37 * Updated and extended "isar-ref" manual, reduced remaining material |
37 in old "ref" manual. |
38 in old "ref" manual. |
|
39 |
|
40 * Improved support for auxiliary contexts indicate block structure for |
|
41 specifications: nesting of "context fixes ... context assumes ..." |
|
42 and "class ... context ...". |
38 |
43 |
39 |
44 |
40 *** Pure *** |
45 *** Pure *** |
41 |
46 |
42 * Code generation for Haskell: restrict unqualified imports from |
47 * Code generation for Haskell: restrict unqualified imports from |