NEWS
changeset 60406 12cc54fac9b0
parent 60404 422b63ef0147
child 60408 1fd46ced2fa8
     1.1 --- a/NEWS	Tue Jun 09 15:28:06 2015 +0200
     1.2 +++ b/NEWS	Tue Jun 09 16:07:11 2015 +0200
     1.3 @@ -7,14 +7,20 @@
     1.4  New in this Isabelle version
     1.5  ----------------------------
     1.6  
     1.7 +*** Isar ***
     1.8 +
     1.9 +* Command 'obtain' binds term abbreviations (via 'is' patterns) in the
    1.10 +proof body as well, abstracted over relevant parameters.
    1.11 +
    1.12 +* Local goal statements (commands 'have', 'show', 'hence', 'thus') allow
    1.13 +an optional context of local variables ('for' declaration).
    1.14 +
    1.15 +* New command 'supply' supports fact definitions during goal refinement
    1.16 +('apply' scripts).
    1.17 +
    1.18 +
    1.19  *** Pure ***
    1.20  
    1.21 -* Isar command 'obtain' binds term abbreviations (via 'is' patterns) in
    1.22 -the proof body as well, abstracted over relevant parameters.
    1.23 -
    1.24 -* New Isar command 'supply' supports fact definitions during goal
    1.25 -refinement ('apply' scripts).
    1.26 -
    1.27  * Configuration option rule_insts_schematic has been discontinued
    1.28  (intermediate legacy feature in Isabelle2015).  INCOMPATIBILITY.
    1.29