# HG changeset patch
# User wenzelm
# Date 1005603925 -3600
# Node ID 04c98351f9af28f8e323a362fec46a0bd86e6b41
# Parent  7c74a52da1102c11525d024e5ce8f45610132e5b
Isar: 'induct' proper support for mutual induction involving
  non-atomic rule statements;
Isar/Pure: support multiple simultaneous goal statements;

diff -r 7c74a52da110 -r 04c98351f9af NEWS
--- a/NEWS	Mon Nov 12 20:23:24 2001 +0100
+++ b/NEWS	Mon Nov 12 23:25:25 2001 +0100
@@ -62,6 +62,23 @@
 statements; NB: major inductive premises need to be put first, all the
 rest of the goal is passed through the induction;
 
+- 'induct' proper support for mutual induction involving non-atomic
+rule statements (uses the new concept of simultaneous goals, see
+below);
+
+* Pure: support multiple simultaneous goal statements, for example
+"have a: A and b: B" (same for 'theorem' etc.); being a pure
+meta-level mechanism, this acts as if several individual goals had
+been stated separately; in particular common proof methods need to be
+repeated in order to cover all claims; note that a single elimination
+step is *not* sufficient to establish the two conjunctions, so this
+fails:
+
+  assume "A & B" then have A and B ..   (*".." fails*)
+
+better use "obtain" in situations as above; alternative refer to
+multi-step methods like 'auto', 'simp_all', 'blast+' etc.;
+
 * Pure: proper integration with ``locales''; unlike the original
 version by Florian Kammueller, Isar locales package high-level proof
 contexts rather than raw logical ones (e.g. we admit to include