--- a/NEWS Thu Jan 07 10:56:05 1999 +0100
+++ b/NEWS Thu Jan 07 11:08:29 1999 +0100
@@ -12,6 +12,14 @@
constants declared in the same theory;
+*** Proof tools ***
+
+* Provers/Arith/fast_lin_arith.ML contains a functor for creating a decision
+procedure for linear arithmetic. Currently it is used for types `nat' and
+`int' in HOL (see below) but can, should and will be instantiated for other
+types and logics as well.
+
+
*** General ***
* in locales, the "assumes" and "defines" parts may be omitted if empty;
@@ -60,6 +68,8 @@
* the datatype declaration of type T now defines the recursor T_rec;
+* The syntax "if P then x else y" is now available in addition to if(P,x,y).
+
New in Isabelle98-1 (October 1998)
----------------------------------