changeset 60404 | 422b63ef0147 |
parent 60390 | c8384ff11711 |
child 60406 | 12cc54fac9b0 |
--- a/NEWS Tue Jun 09 12:32:01 2015 +0200 +++ b/NEWS Tue Jun 09 13:42:58 2015 +0200 @@ -10,7 +10,7 @@ *** Pure *** * Isar command 'obtain' binds term abbreviations (via 'is' patterns) in -the proof body as well, abstracted over the hypothetical parameters. +the proof body as well, abstracted over relevant parameters. * New Isar command 'supply' supports fact definitions during goal refinement ('apply' scripts).