--- 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);