# HG changeset patch
# User wenzelm
# Date 1135208486 -3600
# Node ID a353a61c4544939f4c31a076036d3688ee5555bd
# Parent  4d10150848760dcd52e63e626565ca0c3227dfdb
tuned;

diff -r 4d1015084876 -r a353a61c4544 NEWS
--- a/NEWS	Thu Dec 22 00:29:22 2005 +0100
+++ b/NEWS	Thu Dec 22 00:41:26 2005 +0100
@@ -156,14 +156,14 @@
 of rule sharing the same induction cases.  HOL packages usually
 provide foo_bar.inducts for mutually defined items foo and bar
 (e.g. inductive sets or datatypes).  INCOMPATIBILITY, users need to
-specify mutual induction rules differently, e.g. like this:
+specify mutual induction rules differently, i.e. like this:
 
   (induct rule: foo_bar.inducts)
   (induct set: foo bar)
   (induct type: foo bar)
 
-Moreover, the ML function ProjectRule.projections turns old-style
-rules into the new format.
+The ML function ProjectRule.projections turns old-style rules into the
+new format.
 
 * Provers/induct: support coinduction as well.  See
 src/HOL/Library/Coinductive_List.thy for various examples.