# HG changeset patch
# User nipkow
# Date 938519853 -7200
# Node ID d78b8b103fd908781ddee2499c449826b4347697
# Parent  6680b3b8944b4a4f0bf1dec71d1e48ecbd50018c
incompatibility solver

diff -r 6680b3b8944b -r d78b8b103fd9 NEWS
--- 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 ***