equal
deleted
inserted
replaced
3 |
3 |
4 (Note: Isabelle/jEdit shows a tree-view of the NEWS file in Sidekick.) |
4 (Note: Isabelle/jEdit shows a tree-view of the NEWS file in Sidekick.) |
5 |
5 |
6 New in this Isabelle version |
6 New in this Isabelle version |
7 ---------------------------- |
7 ---------------------------- |
|
8 |
|
9 *** Prover IDE -- Isabelle/Scala/jEdit *** |
|
10 |
|
11 * Command-line invocation "isabelle jedit -R -l LOGIC" opens the ROOT |
|
12 entry of the specified logic session in the editor, while its parent is |
|
13 used for formal checking. |
|
14 |
8 |
15 |
9 *** HOL *** |
16 *** HOL *** |
10 |
17 |
11 * Swapped orientation of congruence rules mod_add_left_eq, |
18 * Swapped orientation of congruence rules mod_add_left_eq, |
12 mod_add_right_eq, mod_add_eq, mod_mult_left_eq, mod_mult_right_eq, |
19 mod_add_right_eq, mod_add_eq, mod_mult_left_eq, mod_mult_right_eq, |
29 with type class annotations. As a result, the tactic that derives |
36 with type class annotations. As a result, the tactic that derives |
30 it no longer fails on nested datatypes. Slight INCOMPATIBILITY. |
37 it no longer fails on nested datatypes. Slight INCOMPATIBILITY. |
31 |
38 |
32 * The theorem in Permutations has been renamed: |
39 * The theorem in Permutations has been renamed: |
33 bij_swap_ompose_bij ~> bij_swap_compose_bij |
40 bij_swap_ompose_bij ~> bij_swap_compose_bij |
34 |
41 |
35 |
42 |
36 New in Isabelle2016-1 (December 2016) |
43 New in Isabelle2016-1 (December 2016) |
37 ------------------------------------- |
44 ------------------------------------- |
38 |
45 |
39 *** General *** |
46 *** General *** |
89 instances) are generated into companion object of corresponding type |
96 instances) are generated into companion object of corresponding type |
90 class, to resolve some situations where ambiguities may occur. |
97 class, to resolve some situations where ambiguities may occur. |
91 |
98 |
92 * Solve direct: option "solve_direct_strict_warnings" gives explicit |
99 * Solve direct: option "solve_direct_strict_warnings" gives explicit |
93 warnings for lemma statements with trivial proofs. |
100 warnings for lemma statements with trivial proofs. |
|
101 |
94 |
102 |
95 *** Prover IDE -- Isabelle/Scala/jEdit *** |
103 *** Prover IDE -- Isabelle/Scala/jEdit *** |
96 |
104 |
97 * More aggressive flushing of machine-generated input, according to |
105 * More aggressive flushing of machine-generated input, according to |
98 system option editor_generated_input_delay (in addition to existing |
106 system option editor_generated_input_delay (in addition to existing |