--- 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)