* 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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
