--- a/NEWS Tue Jan 05 17:30:07 1999 +0100
+++ b/NEWS Wed Jan 06 13:23:41 1999 +0100
@@ -8,12 +8,9 @@
* HOL: Removed the obsolete syntax "Compl A"; use -A for set complement
-*** Proof tools ***
+* ZF: The con_defs part of an inductive definition may no longer refer to
+ constants declared in the same theory;
-* 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 ***
@@ -53,6 +50,17 @@
string -> unit if you really want to output text without newline;
+*** ZF ***
+
+* new primrec section allows primitive recursive functions to be given
+ directly, as in HOL;
+
+* new tactics induct_tac and exhaust_tac for induction (or case analysis)
+ on a datatype;
+
+* the datatype declaration of type T now defines the recursor T_rec;
+
+
New in Isabelle98-1 (October 1998)
----------------------------------