NEWS
changeset 5047 585fa380df1a
parent 5046 de5eacb7361a
child 5059 dcdb21e53537
     1.1 --- a/NEWS	Thu Jun 18 10:50:16 1998 +0200
     1.2 +++ b/NEWS	Thu Jun 18 10:52:34 1998 +0200
     1.3 @@ -1,3 +1,4 @@
     1.4 +
     1.5  Isabelle NEWS -- history of user-visible changes
     1.6  ================================================
     1.7  
     1.8 @@ -40,6 +41,13 @@
     1.9  * new toplevel commands 'Thm' and 'Thms' for retrieving theorems from
    1.10  the current theory context;
    1.11  
    1.12 +* new toplevel commands `Goal' and `Goalw' that improve upon `goal'
    1.13 +and `goalw': the theory is no longer needed as an explicit argument -
    1.14 +the current theory is used; assumptions are no longer returned at the
    1.15 +ML-level unless one of them starts with ==> or !!; it is recommended
    1.16 +to convert to these new commands using isatool fixgoal (as usual,
    1.17 +backup your sources first!);
    1.18 +
    1.19  * new theory section 'nonterminals';
    1.20  
    1.21  * new theory section 'setup';