[isabelle-dev] NEWS: auxiliary contexts
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
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