On Thu, 2 Apr 2015, Peter Lammich wrote:
On Do, 2015-04-02 at 00:16 +0200, Makarius wrote:
* The main operations to certify logical entities are Thm.ctyp_of and
Thm.cterm_of with a local context;
Does this mean that you added functionality concerning the local context
to the Isabelle kernel, which formerly did not know anything about local
contexts?
No, there is no fundamental change. Certification is a matter of the
background theory of the context (the expansion of abbreviations is merely
a historical accident).
The change mainly avoids awkward use of Proof_Context.theory_of in regular
Isabelle/ML sources -- it used to cause confusion about what the real
context is. By keeping theory values mostly out of user core, the risk of
chaos caused by global context vs. the normal local one is reduced --
hopefully.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
