1.1 --- a/NEWS	Sat Apr 14 23:52:17 2012 +0100
     1.2 +++ b/NEWS	Sun Apr 15 13:15:14 2012 +0200
     1.3 @@ -50,6 +50,30 @@
     1.4  
     1.5  *** Pure ***
     1.6  
     1.7 +* Auxiliary contexts indicate block structure for specifications with
     1.8 +additional parameters and assumptions.  Such unnamed contexts may be
     1.9 +nested within other targets, like 'theory', 'locale', 'class',
    1.10 +'instantiation' etc.  Results from the local context are generalized
    1.11 +accordingly and applied to the enclosing target context.  Example:
    1.12 +
    1.13 +  context
    1.14 +    fixes x y z :: 'a
    1.15 +    assumes xy: "x = y" and yz: "y = z"
    1.16 +  begin
    1.17 +
    1.18 +  lemma my_trans: "x = z" using xy yz by simp
    1.19 +
    1.20 +  end
    1.21 +
    1.22 +  thm my_trans
    1.23 +
    1.24 +The most basic application is to factor-out context elements of
    1.25 +several fixes/assumes/shows theorem statements, e.g. see
    1.26 +~~/src/HOL/Isar_Examples/Group_Context.thy
    1.27 +
    1.28 +Any other local theory specification element works within the "context
    1.29 +... begin ... end" block as well.
    1.30 +
    1.31  * Rule composition via attribute "OF" (or ML functions OF/MRS) is more
    1.32  tolerant against multiple unifiers, as long as the final result is
    1.33  unique.  (As before, rules are composed in canonical right-to-left