NEWS

 
 Here the 'fixing: thesis' specification essentially modifies the scope
 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
     shows "P n" and "Q n"
   proof (induct n)

     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, 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.
 
 * Input syntax now supports dummy variable binding "%_. b", where the