|
1 |
1 Isabelle NEWS -- history user-relevant changes |
2 Isabelle NEWS -- history user-relevant changes |
2 ============================================== |
3 ============================================== |
3 |
4 |
4 *** Overview of INCOMPATIBILITIES *** |
5 *** Overview of INCOMPATIBILITIES *** |
5 |
6 |
6 * HOL/Real: "rinv" and "hrinv" replaced by overloaded "inverse" |
7 * HOL/Real: "rinv" and "hrinv" replaced by overloaded "inverse" |
7 function; |
8 operation; |
8 |
9 |
9 * HOL: induct renamed to lfp_induct; |
10 * HOL: induct renamed to lfp_induct; |
10 |
11 |
11 * HOL: contrapos, contrapos2 renamed to contrapos_nn, contrapos_pp; |
12 * HOL: contrapos, contrapos2 renamed to contrapos_nn, contrapos_pp; |
12 |
13 |
13 * HOL: infix "dvd" now has priority 50 rather than 70 |
14 * HOL: infix "dvd" now has priority 50 rather than 70 (because it is a |
14 (because it is a relation) |
15 relation); infix "^^" has been renamed "``"; infix "``" has been |
15 infix ^^ has been renamed `` |
16 renamed "`"; "univalent" has been renamed "single_valued"; |
16 infix `` has been renamed ` |
17 |
17 "univalent" has been renamed "single_valued" |
18 * HOLCF: infix "`" has been renamed "$"; |
18 |
|
19 * HOLCF: infix ` has been renamed $ |
|
20 |
19 |
21 * Isar: 'obtain' no longer declares "that" fact as simp/intro; |
20 * Isar: 'obtain' no longer declares "that" fact as simp/intro; |
22 |
21 |
23 * Isar/HOL: method 'induct' now handles non-atomic goals; as a |
22 * Isar/HOL: method 'induct' now handles non-atomic goals; as a |
24 consequence, it is no longer monotonic wrt. the local goal context |
23 consequence, it is no longer monotonic wrt. the local goal context |
29 |
28 |
30 * improved isabelle style files; more abstract symbol implementation |
29 * improved isabelle style files; more abstract symbol implementation |
31 (should now use \isamath{...} and \isatext{...} in custom symbol |
30 (should now use \isamath{...} and \isatext{...} in custom symbol |
32 definitions); |
31 definitions); |
33 |
32 |
|
33 * \isabellestyle{NAME} selects version of Isabelle output (currently |
|
34 available: are "it" for near math-mode best-style output, "sl" for |
|
35 slanted text style, and "tt" for plain type-writer; if no |
|
36 \isabellestyle command is given, output is according to slanted |
|
37 type-writer); |
|
38 |
34 * support sub/super scripts (for single symbols only), input syntax is |
39 * support sub/super scripts (for single symbols only), input syntax is |
35 like this: "A\<^sup>*" or "A\<^sup>\<star>"; |
40 like this: "A\<^sup>*" or "A\<^sup>\<star>"; |
|
41 |
|
42 * some more standard symbols; see Appendix A of the system manual for |
|
43 the complete list; |
36 |
44 |
37 * antiquotation @{goals} and @{subgoals} for output of *dynamic* goals |
45 * antiquotation @{goals} and @{subgoals} for output of *dynamic* goals |
38 state; Note that presentation of goal states does not conform to |
46 state; Note that presentation of goal states does not conform to |
39 actual human-readable proof documents. Please do not include goal |
47 actual human-readable proof documents. Please do not include goal |
40 states into document output unless you really know what you are doing! |
48 states into document output unless you really know what you are doing! |
60 instance proofs may be performed by ".."; |
68 instance proofs may be performed by ".."; |
61 |
69 |
62 * Pure: ?thesis / ?this / "..." now work for pure meta-level |
70 * Pure: ?thesis / ?this / "..." now work for pure meta-level |
63 statements as well; |
71 statements as well; |
64 |
72 |
|
73 * Pure: the builtin notion of 'finished' goal now includes the ==-refl |
|
74 rule (as well as the assumption rule); |
|
75 |
|
76 * Pure: 'thm_deps' command visualizes dependencies of theorems and |
|
77 lemmas, using the graph browser tool; |
|
78 |
65 * HOL: improved method 'induct' --- now handles non-atomic goals |
79 * HOL: improved method 'induct' --- now handles non-atomic goals |
66 (potential INCOMPATIBILITY); tuned error handling; |
80 (potential INCOMPATIBILITY); tuned error handling; |
67 |
81 |
68 * HOL: cases and induct rules now provide explicit hints about the |
82 * HOL: cases and induct rules now provide explicit hints about the |
69 number of facts to be consumed (0 for "type" and 1 for "set" rules); |
83 number of facts to be consumed (0 for "type" and 1 for "set" rules); |
70 any remaining facts are inserted into the goal verbatim; |
84 any remaining facts are inserted into the goal verbatim; |
|
85 |
|
86 * HOL: local contexts (aka cases) may now contain term bindings as |
|
87 well; the 'cases' and 'induct' methods new provide a ?case binding for |
|
88 the result to be shown in each case; |
71 |
89 |
72 * HOL: added 'recdef_tc' command; |
90 * HOL: added 'recdef_tc' command; |
73 |
91 |
74 |
92 |
75 *** HOL *** |
93 *** HOL *** |
89 |
107 |
90 * HOL-Hyperreal: a new target, extending HOL-Real with the hyperreals and |
108 * HOL-Hyperreal: a new target, extending HOL-Real with the hyperreals and |
91 Fleuriot's mechanization of analysis; |
109 Fleuriot's mechanization of analysis; |
92 |
110 |
93 * HOL-Real, HOL-Hyperreals: improved arithmetic simplification; |
111 * HOL-Real, HOL-Hyperreals: improved arithmetic simplification; |
|
112 |
94 |
113 |
95 *** CTT *** |
114 *** CTT *** |
96 |
115 |
97 * CTT: x-symbol support for Pi, Sigma, -->, : (membership); note that |
116 * CTT: x-symbol support for Pi, Sigma, -->, : (membership); note that |
98 "lam" is displayed as TWO lambda-symbols |
117 "lam" is displayed as TWO lambda-symbols |