Thu, 22 Dec 2005 00:41:26 +0100
changeset 18488 a353a61c4544
parent 18487 4d1015084876
child 18489 151e52a4db3f
--- 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.