--- a/NEWS Tue Sep 28 13:37:54 1999 +0200
+++ b/NEWS Tue Sep 28 13:57:33 1999 +0200
@@ -1,4 +1,3 @@
-
Isabelle NEWS -- history user-relevant changes
==============================================
@@ -30,6 +29,12 @@
* HOL/List: the constructors of type list are now Nil and Cons;
+* Simplifier: the type of the infix ML functions
+ setSSolver addSSolver setSolver addSolver
+is now simpset * solver -> simpset where `solver' is a new abstract type
+for packaging solvers. A solver is created via
+ mk_solver: string -> (thm list -> int -> tactic) -> solver
+where the string argument is only a comment.
*** Proof tools ***