equal
deleted
inserted
replaced
10 * HOL: Removed the obsolete syntax "Compl A"; use -A for set complement |
10 * HOL: Removed the obsolete syntax "Compl A"; use -A for set complement |
11 |
11 |
12 *** General *** |
12 *** General *** |
13 |
13 |
14 * in locales, the "assumes" and "defines" parts may be omitted if empty; |
14 * in locales, the "assumes" and "defines" parts may be omitted if empty; |
|
15 |
|
16 * new print_mode "xsymbols" for extended symbol support |
|
17 (e.g. genuiely long arrows) |
|
18 |
15 |
19 |
16 *** Internal programming interfaces *** |
20 *** Internal programming interfaces *** |
17 |
21 |
18 * tuned current_goals_markers semantics: begin / end goal avoids |
22 * tuned current_goals_markers semantics: begin / end goal avoids |
19 printing empty lines; |
23 printing empty lines; |