Re: [isabelle-dev] NEWS: Thm.cterm_of and Thm.ctyp_of operate on local context
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-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Thm.cterm_of and Thm.ctyp_of operate on local context
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, which formerly did not know anything about local contexts? 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. By keeping theory values mostly out of user core, the risk of chaos caused by global context vs. the normal local one is reduced -- hopefully. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Thm.cterm_of and Thm.ctyp_of operate on local context
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; It is immediately clear what it does, and that there is no problem with it. This mail thread could have been shortened by posting the ML definition earlier. But the main thing is not the kernel here, it is user ML code that is a bit outdated concerning proper use of context. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Thm.cterm_of and Thm.ctyp_of operate on local context
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
