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
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,
On Thu, 2 Apr 2015, Peter Lammich wrote:
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.
The kernel is not affected by a line like this:
val cterm_of = global_cterm_of o Proof_Context.theory_of;
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
