changeset 60387 | 76359ff1090f |
parent 60371 | 8a5cfdda1b98 |
child 60390 | c8384ff11711 |
--- a/NEWS Mon Jun 08 14:45:31 2015 +0200 +++ b/NEWS Mon Jun 08 19:38:08 2015 +0200 @@ -9,6 +9,9 @@ *** Pure *** +* Isar command 'obtain' binds term abbreviations (via 'is' patterns) in +the proof body as well, abstracted over hypothetical parameters. + * New Isar command 'supply' supports fact definitions during goal refinement ('apply' scripts).