equal
deleted
inserted
replaced
6 |
6 |
7 New in this Isabelle version |
7 New in this Isabelle version |
8 ---------------------------- |
8 ---------------------------- |
9 |
9 |
10 *** Pure *** |
10 *** Pure *** |
|
11 |
|
12 * Isar command 'obtain' binds term abbreviations (via 'is' patterns) in |
|
13 the proof body as well, abstracted over hypothetical parameters. |
11 |
14 |
12 * New Isar command 'supply' supports fact definitions during goal |
15 * New Isar command 'supply' supports fact definitions during goal |
13 refinement ('apply' scripts). |
16 refinement ('apply' scripts). |
14 |
17 |
15 * Configuration option rule_insts_schematic has been discontinued |
18 * Configuration option rule_insts_schematic has been discontinued |