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