[isabelle-dev] NEWS: auxiliary contexts

Makarius makarius at sketis.net
Sun Apr 15 14:54:54 CEST 2012

* 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:

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

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


   thm my_trans

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

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 

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

Please report your experience with it.


More information about the isabelle-dev mailing list