equal
deleted
inserted
replaced
9 |
9 |
10 *** Isar *** |
10 *** Isar *** |
11 |
11 |
12 * Command 'obtain' binds term abbreviations (via 'is' patterns) in the |
12 * Command 'obtain' binds term abbreviations (via 'is' patterns) in the |
13 proof body as well, abstracted over relevant parameters. |
13 proof body as well, abstracted over relevant parameters. |
|
14 |
|
15 * Term abbreviations via 'is' patterns also work for schematic |
|
16 statements: result is abstracted over unknowns. |
14 |
17 |
15 * Local goal statements (commands 'have', 'show', 'hence', 'thus') allow |
18 * Local goal statements (commands 'have', 'show', 'hence', 'thus') allow |
16 an optional context of local variables ('for' declaration). |
19 an optional context of local variables ('for' declaration). |
17 |
20 |
18 * New command 'supply' supports fact definitions during goal refinement |
21 * New command 'supply' supports fact definitions during goal refinement |