# HG changeset patch
# User nipkow
# Date 898080242 -7200
# Node ID 59808d00ea8da3124faaaa5531b58ebe829c435d
# Parent  3fdc881e8ff9c19288b5da1dd689d570a5372721
Goal and Goalw

diff -r 3fdc881e8ff9 -r 59808d00ea8d NEWS
--- a/NEWS	Wed Jun 17 10:49:45 1998 +0200
+++ b/NEWS	Wed Jun 17 12:44:02 1998 +0200
@@ -1,4 +1,3 @@
-
 Isabelle NEWS -- history of user-visible changes
 ================================================
 
@@ -29,6 +28,12 @@
   delWrapper, delSWrapper: claset *  string            -> claset
   getWrapper is renamed to appWrappers, getSWrapper to appSWrappers;
 
+* new toplevel commands `Goal' and `Goalw' that improve upon `goal' and
+`goalw': the theory is no longer needed as an explicit argument - the current
+theory is used; assumptions are no longer returned at the ML-level unless one
+of them starts with ==> or !!. It is recommended to convert to these new
+commands.
+
 * inductive definitions now handle disjunctive premises correctly (HOL
 and ZF);