diff -r d275fd349f3d -r 0afcae75b34a NEWS
--- a/NEWS	Tue Apr 28 13:52:18 1998 +0200
+++ b/NEWS	Wed Apr 29 11:10:40 1998 +0200
@@ -1,58 +1,64 @@
+
 Isabelle NEWS -- history of user-visible changes
 ================================================
 
 New in Isabelle??? (FIXME)
 --------------------------
 
-* Changed wrapper mechanism for the classical reasoner now allows for selected
-  deletion of wrappers, by introduction of names for wrapper functionals.
-  This implies that addbefore, addSbefore, addaltern, and addSaltern now take
-  a pair (name, tactic) as argument, and that adding two tactics with the same
-  name overwrites the first one (emitting a warning).
+*** General Changes ***
+
+* Changed wrapper mechanism for the classical reasoner now allows for
+selected deletion of wrappers, by introduction of names for wrapper
+functionals.  This implies that addbefore, addSbefore, addaltern, and
+addSaltern now take a pair (name, tactic) as argument, and that adding
+two tactics with the same name overwrites the first one (emitting a
+warning).
   type wrapper = (int -> tactic) -> (int -> tactic)
   setWrapper, setSWrapper, compWrapper and compSWrapper are replaced by
   addWrapper, addSWrapper: claset * (string * wrapper) -> claset
   delWrapper, delSWrapper: claset *  string            -> claset
   getWrapper is renamed to appWrappers, getSWrapper to appSWrappers;
 
-* Inductive definitions now handle disjunctive premises correctly (HOL and ZF)
+* inductive definitions now handle disjunctive premises correctly (HOL
+and ZF);
+
+* new toplevel commands 'thm' and 'thms' for retrieving theorems from
+the current theory context;
 
 
 *** HOL ***
 
-* new force_tac (and its derivations Force_tac, force) 
-  combines rewriting and classical reasoning (and whatever other tools)
-  similarly to auto_tac, but is aimed to solve the given subgoal totally.
+* new force_tac (and its derivations Force_tac, force): combines
+rewriting and classical reasoning (and whatever other tools) similarly
+to auto_tac, but is aimed to solve the given subgoal totally;
 
 * added option_map_eq_Some to simpset() and claset()
 
 * New directory HOL/UNITY: Chandy and Misra's UNITY formalism
 
-* split_all_tac is now much faster and fails if there is nothing to split.
-  Existing (fragile) proofs may require adaption because the order and the
-  names of the automatically generated variables have changed.
-  split_all_tac has moved within claset() from usafe wrappers to safe wrappers,
-  which means that !!-bound variables are splitted much more aggressively,
-  and safe_tac and clarify_tac now split such variables.
-  If this splitting is not appropriate, use delSWrapper "split_all_tac".
+* split_all_tac is now much faster and fails if there is nothing to
+split.  Existing (fragile) proofs may require adaption because the
+order and the names of the automatically generated variables have
+changed.  split_all_tac has moved within claset() from usafe wrappers
+to safe wrappers, which means that !!-bound variables are splitted
+much more aggressively, and safe_tac and clarify_tac now split such
+variables.  If this splitting is not appropriate, use delSWrapper
+"split_all_tac".
 
-* added disj_not1 = "(~P | Q) = (P --> Q)" to the default simpset
+* added disj_not1 = "(~P | Q) = (P --> Q)" to the default simpset;
 
-* HOL/Arithmetic
+* HOL/Arithmetic:
   
   - removed 'pred' (predecessor) function
-
   - generalized some theorems about n-1
-
   - Many new laws about "div" and "mod"
-
   - New laws about greatest common divisors (see theory ex/Primes)
 
-* HOL/Relation: renamed the relational operatotr r^-1 "converse" instead of
-  "inverse"
+* HOL/Relation: renamed the relational operatotr r^-1 "converse"
+instead of "inverse";
 
-* recdef can now declare non-recursive functions, with {} supplied as the 
-  well-founded relation
+* recdef can now declare non-recursive functions, with {} supplied as
+the well-founded relation;
 
 * Simplifier:
 
@@ -87,6 +93,7 @@
 * many new identities for unions, intersections, set difference, etc.;
 
 
+
 New in Isabelle98 (January 1998)
 --------------------------------