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

[Peter Lammich]

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?

--
  Peter


> 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
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev