# HG changeset patch
# User wenzelm
# Date 898159954 -7200
# Node ID 585fa380df1a4f217ea23a213e9ecd82e2850b2a
# Parent  de5eacb7361af3de9c73f4988dc999609d264b6b
new toplevel commands `Goal' and `Goalw';
isatool fixgoal;

diff -r de5eacb7361a -r 585fa380df1a NEWS
--- 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';