# HG changeset patch
# User paulson
# Date 898677222 -7200
# Node ID 9a3d48fa28cac496e34545c609e346bda437e44d
# Parent  753d4daff1dfd7cab66531e282f55cd383e7425a
removed duplicate entry for Goal

diff -r 753d4daff1df -r 9a3d48fa28ca NEWS
--- a/NEWS	Wed Jun 24 10:30:29 1998 +0200
+++ b/NEWS	Wed Jun 24 10:33:42 1998 +0200
@@ -7,9 +7,14 @@
 
 *** General Changes ***
 
-* Simplifier:
+* 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!);
 
- -Asm_full_simp_tac is now more aggressive:
+* Simplifier: Asm_full_simp_tac is now more aggressive.
   1. It will sometimes reorient premises if that increases their power to
      simplify.
   2. It does no longer proceed strictly from left to right but may also
@@ -29,25 +34,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);
 
 * 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';