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