# HG changeset patch
# User wenzelm
# Date 1005686759 -3600
# Node ID b1c16d685a99e055b8a95ba9ab28fc2ff36c9b7b
# Parent  f9139e09a98331698908edb21a707c308cb7ac34
* ZF: new-style theory commands 'inductive', 'inductive_cases', and
methods 'ind_cases', 'induct_tac', 'case_tac';

diff -r f9139e09a983 -r b1c16d685a99 NEWS
--- a/NEWS	Tue Nov 13 22:24:28 2001 +0100
+++ b/NEWS	Tue Nov 13 22:25:59 2001 +0100
@@ -209,14 +209,17 @@
 
 *** ZF ***
 
+* ZF: new-style theory commands 'inductive', 'inductive_cases', and
+methods 'ind_cases', 'induct_tac', 'case_tac';
+
 * ZF: the integer library now covers quotients and remainders, with
 many laws relating division to addition, multiplication, etc.;
 
-* ZF/Induct: new directory for examples of inductive definitions, including theory
-Multiset for multiset orderings;
-
-* ZF/UNITY: Chandy and Misra's UNITY is now available in ZF, giving a typeless
-version of the formalism;
+* ZF/Induct: new directory for examples of inductive definitions,
+including theory Multiset for multiset orderings;
+
+* ZF/UNITY: Chandy and Misra's UNITY is now available in ZF, giving a
+typeless version of the formalism;
 
 
 *** General ***