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