Goal and Goalw
authornipkow
Wed Jun 17 12:44:02 1998 +0200 (1998-06-17)
changeset 504459808d00ea8d
parent 5043 3fdc881e8ff9
child 5045 a19e5c91a1ab
Goal and Goalw
NEWS
     1.1 --- a/NEWS	Wed Jun 17 10:49:45 1998 +0200
     1.2 +++ b/NEWS	Wed Jun 17 12:44:02 1998 +0200
     1.3 @@ -1,4 +1,3 @@
     1.4 -
     1.5  Isabelle NEWS -- history of user-visible changes
     1.6  ================================================
     1.7  
     1.8 @@ -29,6 +28,12 @@
     1.9    delWrapper, delSWrapper: claset *  string            -> claset
    1.10    getWrapper is renamed to appWrappers, getSWrapper to appSWrappers;
    1.11  
    1.12 +* new toplevel commands `Goal' and `Goalw' that improve upon `goal' and
    1.13 +`goalw': the theory is no longer needed as an explicit argument - the current
    1.14 +theory is used; assumptions are no longer returned at the ML-level unless one
    1.15 +of them starts with ==> or !!. It is recommended to convert to these new
    1.16 +commands.
    1.17 +
    1.18  * inductive definitions now handle disjunctive premises correctly (HOL
    1.19  and ZF);
    1.20