# HG changeset patch
# User wenzelm
# Date 1135347493 -3600
# Node ID 96260fb114493b2fe5b977342a919ed90eda4cd1
# Parent  95e6c9ef748817119a5adf4ad35521c936368e41
* Provers/induct: support simultaneous goals with mutual rules;

diff -r 95e6c9ef7488 -r 96260fb11449 NEWS
--- a/NEWS	Fri Dec 23 15:16:58 2005 +0100
+++ b/NEWS	Fri Dec 23 15:18:13 2005 +0100
@@ -127,11 +127,24 @@
 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:
+* 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, i.e. like this:
+
+  (induct rule: foo_bar.inducts)
+  (induct set: foo bar)
+  (induct type: foo bar)
+
+The ML function ProjectRule.projections turns old-style rules into the
+new format.
+
+* Provers/induct: improved handling of simultaneous goals.  Instead of
+introducing object-level conjunction, the statement is now split into
+several conclusions, while the corresponding symbolic cases are
+duplicated accordingly.  INCOMPATIBILITY, proofs need to be structured
+explicitly, e.g. like this:
 
   lemma
     fixes n :: nat
@@ -152,18 +165,17 @@
     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, i.e. like this:
-
-  (induct rule: foo_bar.inducts)
-  (induct set: foo bar)
-  (induct type: foo bar)
-
-The ML function ProjectRule.projections turns old-style rules into the
-new format.
+If simultaneous goals are to be used with mutual rules, the statement
+needs to be structured carefully as a two-level conjunction, using
+lists of propositions separated by 'and':
+
+lemma
+  shows "a : A ==> P1 a"
+        "a : A ==> P2 a"
+    and "b : B ==> Q1 b"
+        "b : B ==> Q2 b"
+        "b : B ==> Q3 b"
+proof (induct set: A B)
 
 * Provers/induct: support coinduction as well.  See
 src/HOL/Library/Coinductive_List.thy for various examples.