# HG changeset patch
# User wenzelm
# Date 1135207752 -3600
# Node ID 8ac97f71369d58fd7efe363598d02ea6281b081c
# Parent  82707239f377b79ab58988ab44fe831b80dad7d1
* induct: improved treatment of mutual goals and mutual rules;

diff -r 82707239f377 -r 8ac97f71369d NEWS
--- a/NEWS	Thu Dec 22 00:29:11 2005 +0100
+++ b/NEWS	Thu Dec 22 00:29:12 2005 +0100
@@ -127,6 +127,44 @@
 of the formal thesis parameter, in order to the get the whole
 existence statement through the induction as expected.
 
+* Provers/induct: mutual goals no longer result in object-level
+conjunction, but in properly split meta-level statements,
+INCOMPATIBILITY.  The corresponding cases are duplicated accordingly,
+with the case names being indexed according to the number of
+conjuncts.  For example:
+
+  lemma
+    fixes n :: nat
+    shows "P n" and "Q n"
+  proof (induct n)
+    case 01
+    show "P 0" sorry
+  next
+    case 02
+    show "Q 0" sorry
+  next
+    case (Suc1 n)
+    note `P n` and `Q n`
+    show "P (Suc n)" sorry
+  next
+    case (Suc2 n)
+    note `P n` and `Q n`
+    show "Q (Suc n)" sorry
+  qed
+
+* Provers/induct: mutual induction rules are now specified as a list
+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:
+
+  (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.
+
 * Provers/induct: support coinduction as well.  See
 src/HOL/Library/Coinductive_List.thy for various examples.
 
@@ -157,6 +195,9 @@
 "=" on type bool) are handled, variable names of the form "lit_<n>"
 are no longer reserved, significant speedup.
 
+* inductive and datatype: provide projections of mutual rules, bundled
+as foo_bar.inducts;
+
 * Library: added theory Coinductive_List of potentially infinite lists
 as greatest fixed-point.