NEWS
changeset 61733 00fcff12c59f
parent 61729 30d4ccd54861
child 61748 fc53fbf9fe01
     1.1 --- a/NEWS	Sat Nov 21 23:02:12 2015 +0100
     1.2 +++ b/NEWS	Sun Nov 22 13:33:38 2015 +0100
     1.3 @@ -155,8 +155,8 @@
     1.4  statements: result is abstracted over unknowns.
     1.5  
     1.6  * Local goals ('have', 'show', 'hence', 'thus') allow structured
     1.7 -statements like fixes/assumes/shows in theorem specifications, but the
     1.8 -notation is postfix with keywords 'if' (or 'when') and 'for'. For
     1.9 +rule statements like fixes/assumes/shows in theorem specifications, but
    1.10 +the notation is postfix with keywords 'if' (or 'when') and 'for'. For
    1.11  example:
    1.12  
    1.13    have result: "C x y"
    1.14 @@ -178,8 +178,8 @@
    1.15  The keyword 'when' may be used instead of 'if', to indicate 'presume'
    1.16  instead of 'assume' above.
    1.17  
    1.18 -* Assumptions ('assume', 'presume') allow structured statements using
    1.19 -'if' and 'for', similar to 'have' etc. above. For example:
    1.20 +* Assumptions ('assume', 'presume') allow structured rule statements
    1.21 +using 'if' and 'for', similar to 'have' etc. above. For example:
    1.22  
    1.23    assume result: "C x y"
    1.24      if "A x" and "B y"