# HG changeset patch
# User paulson
# Date 915625421 -3600
# Node ID 0786b5afd8eebd8490435723b121c69c85a7e995
# Parent  aa2ac7d217921decc61909a78d2617f13ad924b6
primrec, induct_tac

diff -r aa2ac7d21792 -r 0786b5afd8ee NEWS
--- 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)
 ----------------------------------