diff -r 1ad3866b86cc -r 2ceddd91cd0a NEWS
--- a/NEWS	Wed Sep 29 14:36:04 1999 +0200
+++ b/NEWS	Wed Sep 29 14:36:36 1999 +0200
@@ -36,6 +36,7 @@
 	mk_solver: string -> (thm list -> int -> tactic) -> solver
 where the string argument is only a comment.
 
+
 *** Proof tools ***
 
 * Provers/Arith/fast_lin_arith.ML contains a functor for creating a
@@ -288,6 +289,12 @@
 your own database of information attached to *whole* theories -- as
 opposed to intra-theory data slots offered via TheoryDataFun;
 
+* proper handling of dangling sort hypotheses (at last!);
+Thm.strip_shyps and Drule.strip_shyps_warning take care of removing
+extra sort hypotheses that can be witnessed from the type signature;
+the force_strip_shyps is gone, any remaining shyps are simply left in
+the theorem (with a warning issued by strip_shyps_warning);
+
 
 
 New in Isabelle98-1 (October 1998)