[isabelle-dev] NEWS: Thm.cterm_of and Thm.ctyp_of operate on local context
lammich at in.tum.de
Thu Apr 2 19:02:52 CEST 2015
> 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.
So what is the reason not to put it in more_thm.ML?
There, it would not affect the kernel itself, and still appear as
Thm.cterm_of to the user.
More information about the isabelle-dev