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

[Makarius]

* The main operations to certify logical entities are Thm.ctyp_of and
Thm.cterm_of with a local context; old-style global theory variants are
available as Thm.global_ctyp_of and Thm.global_cterm_of.
INCOMPATIBILITY.


This refers to Isabelle/291934bac95e -- yet another step in the 
localization project.

There is a tiny semantic snag: both the local and global operations expand 
abbreviations from the *global* background theory.  Mayne they should not 
do anything like that at all, and leave changes to the types/terms to the 
canonical "check" phases.  But that is another reform, another time.


Hardly any values (thy: theory) should now show up in regular Isabelle/ML 
tool implementations.  People who still think they don't understand proper 
(ctxt: Proof.context) things, should practise more of the art of mental 
abstraction -- and look at good examples in the Isabelle code base.


 	Makarius