--- a/NEWS Thu Jun 18 10:50:16 1998 +0200
+++ b/NEWS Thu Jun 18 10:52:34 1998 +0200
@@ -1,3 +1,4 @@
+
Isabelle NEWS -- history of user-visible changes
================================================
@@ -40,6 +41,13 @@
* new toplevel commands 'Thm' and 'Thms' for retrieving theorems from
the current theory context;
+* 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 using isatool fixgoal (as usual,
+backup your sources first!);
+
* new theory section 'nonterminals';
* new theory section 'setup';