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