diff -r 4074c7d86d44 -r b3d18eb3ac20 NEWS
--- a/NEWS	Wed Jul 01 19:03:54 1998 +0200
+++ b/NEWS	Wed Jul 01 19:11:20 1998 +0200
@@ -46,6 +46,20 @@
 
 *** HOL ***
 
+* Inductive definition package: Mutually recursive definitions such as
+
+  inductive EVEN ODD
+    intrs
+      null " 0 : EVEN"
+      oddI "n : EVEN ==> Suc n : ODD"
+      evenI "n : ODD ==> Suc n : EVEN"
+
+  are now possible. Theories containing (co)inductive definitions must now
+  have theory "Inductive" as an ancestor. The new component "elims" of the
+  structure created by the package contains an elimination rule for each of
+  the recursive sets. Note that the component "mutual_induct" no longer
+  exists - the induction rule is always contained in "induct".
+
 * HOL/Real: a construction of the reals using Dedekind cuts
 
 * HOL/record: now includes concrete syntax for record terms (still