[isabelle-dev] NEWS: Thm.cterm_of and Thm.ctyp_of operate on local context

[Makarius]

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