[isabelle-dev] NEWS: auxiliary contexts

[Makarius]

* Auxiliary contexts indicate block structure for specifications with
additional parameters and assumptions.  Such unnamed contexts may be
nested within other targets, like 'theory', 'locale', 'class',
'instantiation' etc.  Results from the local context are generalized
accordingly and applied to the enclosing target context.  Example:

   context
     fixes x y z :: 'a
     assumes xy: "x = y" and yz: "y = z"
   begin

   lemma my_trans: "x = z" using xy yz by simp

   end

   thm my_trans

The most basic application is to factor-out context elements of
several fixes/assumes/shows theorem statements, e.g. see
~/src/HOL/Isar_Examples/Group_Context.thy

Any other local theory specification element works within the "context
... begin ... end" block as well.


This refers to Isabelle/a83b25e5bad3.  The idea has been in the pipeline 
since about 2007/2008, but we could not afford it so far due to national 
debts.

There might be some rough edges still in the implementation, which are 
hopefully ironed out until the release.

Please report your experience with it.


 	Makarius