equal
deleted
inserted
replaced
18 - "chapter_definition NAME (GROUPS)" to make all sessions that belong |
18 - "chapter_definition NAME (GROUPS)" to make all sessions that belong |
19 to this chapter members of the given groups |
19 to this chapter members of the given groups |
20 |
20 |
21 - "chapter_definition NAME description TEXT" to provide a description |
21 - "chapter_definition NAME description TEXT" to provide a description |
22 for presentation purposes |
22 for presentation purposes |
|
23 |
|
24 * The instantiation of schematic goals is now displayed explicitly as a |
|
25 list of variable assignments. This works for proof state output, and at |
|
26 the end of a toplevel proof. In rare situations, a proof command or |
|
27 proof method may violate the intended goal discipline, by not producing |
|
28 an instance of the original goal, but there is only a warning, no hard |
|
29 error. |
23 |
30 |
24 * System option "show_states" controls output of toplevel command states |
31 * System option "show_states" controls output of toplevel command states |
25 (notably proof states) in batch-builds; in interactive mode this is |
32 (notably proof states) in batch-builds; in interactive mode this is |
26 always done on demand. The option is relevant for tools that operate on |
33 always done on demand. The option is relevant for tools that operate on |
27 exported PIDE markup, e.g. document presentation or diagnostics. For |
34 exported PIDE markup, e.g. document presentation or diagnostics. For |