# HG changeset patch
# User paulson
# Date 915703709 -3600
# Node ID a99879bd9f1344565c3b24ebc5c54dfa088519ec
# Parent  2d8f3e1f1151e87269f7682d573cb9cd06a39783
if-then-else syntax for ZF

diff -r 2d8f3e1f1151 -r a99879bd9f13 NEWS
--- 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)
 ----------------------------------