NEWS
changeset 60414 f25f2f2ba48c
parent 60408 1fd46ced2fa8
child 60418 0bcffc47eaca
     1.1 --- a/NEWS	Wed Jun 10 11:52:54 2015 +0200
     1.2 +++ b/NEWS	Wed Jun 10 14:46:31 2015 +0200
     1.3 @@ -15,8 +15,25 @@
     1.4  * Term abbreviations via 'is' patterns also work for schematic
     1.5  statements: result is abstracted over unknowns.
     1.6  
     1.7 -* Local goal statements (commands 'have', 'show', 'hence', 'thus') allow
     1.8 -an optional context of local variables ('for' declaration).
     1.9 +* Local goals ('have', 'show', 'hence', 'thus') allow structured
    1.10 +statements like fixes/assumes/shows in theorem specifications, but the
    1.11 +notation is postfix with keywords 'if' and 'for'. For example:
    1.12 +
    1.13 +  have result: "C x y"
    1.14 +    if "A x" and "B y"
    1.15 +    for x :: 'a and y :: 'a
    1.16 +    <proof>
    1.17 +
    1.18 +The local assumptions are always bound to the name "prems".  The result
    1.19 +is exported from context of the statement as usual.  The above roughly
    1.20 +corresponds to a raw proof block like this:
    1.21 +
    1.22 +  {
    1.23 +    fix x :: 'a and y :: 'a
    1.24 +    assume prems: "A x" "B y"
    1.25 +    have "C x y" <proof>
    1.26 +  }
    1.27 +  note result = this
    1.28  
    1.29  * New command 'supply' supports fact definitions during goal refinement
    1.30  ('apply' scripts).