NEWS
changeset 60477 051b200f7578
parent 60460 abee0de69a89
child 60479 db238135f386
     1.1 --- a/NEWS	Sun Jun 14 20:10:21 2015 +0200
     1.2 +++ b/NEWS	Sun Jun 14 23:22:08 2015 +0200
     1.3 @@ -12,6 +12,9 @@
     1.4  * Command 'obtain' binds term abbreviations (via 'is' patterns) in the
     1.5  proof body as well, abstracted over relevant parameters.
     1.6  
     1.7 +* Improved type-inference for theorem statement 'obtains': separate
     1.8 +parameter scope for of each clause.
     1.9 +
    1.10  * Term abbreviations via 'is' patterns also work for schematic
    1.11  statements: result is abstracted over unknowns.
    1.12