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