1 |
1 |
2 Isabelle NEWS -- history user-relevant changes |
2 Isabelle NEWS -- history user-relevant changes |
3 ============================================== |
3 ============================================== |
|
4 |
|
5 New in Isabelle99-2 (February 2001) |
|
6 ----------------------------------- |
4 |
7 |
5 *** Overview of INCOMPATIBILITIES *** |
8 *** Overview of INCOMPATIBILITIES *** |
6 |
9 |
7 * HOL: inductive package no longer splits induction rule aggressively, |
10 * HOL: inductive package no longer splits induction rule aggressively, |
8 but only as far as specified by the introductions given; the old |
11 but only as far as specified by the introductions given; the old |
43 |
46 |
44 * support sub/super scripts (for single symbols only), input syntax is |
47 * support sub/super scripts (for single symbols only), input syntax is |
45 like this: "A\<^sup>*" or "A\<^sup>\<star>"; |
48 like this: "A\<^sup>*" or "A\<^sup>\<star>"; |
46 |
49 |
47 * some more standard symbols; see Appendix A of the system manual for |
50 * some more standard symbols; see Appendix A of the system manual for |
48 the complete list; |
51 the complete list of symbols defined in isabellesym.sty; |
49 |
52 |
50 * improved isabelle style files; more abstract symbol implementation |
53 * improved isabelle style files; more abstract symbol implementation |
51 (should now use \isamath{...} and \isatext{...} in custom symbol |
54 (should now use \isamath{...} and \isatext{...} in custom symbol |
52 definitions); |
55 definitions); |
53 |
56 |
54 * antiquotation @{goals} and @{subgoals} for output of *dynamic* goals |
57 * antiquotation @{goals} and @{subgoals} for output of *dynamic* goals |
55 state; Note that presentation of goal states does not conform to |
58 state; Note that presentation of goal states does not conform to |
56 actual human-readable proof documents. Please do not include goal |
59 actual human-readable proof documents. Please do not include goal |
57 states into document output unless you really know what you are doing! |
60 states into document output unless you really know what you are doing! |
58 |
61 |
59 * isatool unsymbolize tunes sources for plain ASCII communication; |
62 * proper indentation of antiquoted output with proportional LaTeX |
|
63 fonts; |
60 |
64 |
61 * no_document ML operator temporarily disables LaTeX document |
65 * no_document ML operator temporarily disables LaTeX document |
62 generation; |
66 generation; |
|
67 |
|
68 * isatool unsymbolize tunes sources for plain ASCII communication; |
63 |
69 |
64 |
70 |
65 *** Isar *** |
71 *** Isar *** |
66 |
72 |
67 * Pure: Isar now suffers initial goal statements to contain unbound |
73 * Pure: Isar now suffers initial goal statements to contain unbound |
157 *** General *** |
163 *** General *** |
158 |
164 |
159 * print modes "brackets" and "no_brackets" control output of nested => |
165 * print modes "brackets" and "no_brackets" control output of nested => |
160 (types) and ==> (props); the default behaviour is "brackets"; |
166 (types) and ==> (props); the default behaviour is "brackets"; |
161 |
167 |
162 * system: support Poly/ML 4.0 (current beta versions); |
168 * system: support Poly/ML 4.0; |
163 |
169 |
164 * Pure: the Simplifier has been implemented properly as a derived rule |
170 * Pure: the Simplifier has been implemented properly as a derived rule |
165 outside of the actual kernel (at last!); the overall performance |
171 outside of the actual kernel (at last!); the overall performance |
166 penalty in practical applications is about 50%, while reliability of |
172 penalty in practical applications is about 50%, while reliability of |
167 the Isabelle inference kernel has been greatly improved; |
173 the Isabelle inference kernel has been greatly improved; |