See now http://isabelle.in.tum.de/repos/isabelle/rev/e4b5bebe5235.
When following the suggestions of the ML code http://isabelle.in.tum.de/repos/isabelle/file/9e4220605179/src/Pure/Isar/expression.ML#l42 I am personally still in favor of only three Isar keywords, corresponding to permanent_interpretation ephemeral_interpretation interpret with the perspective to generalize permanent_interpretation from named targets to arbitrary targets by means of a dedicated local theory operation, like Local_Theory.subscription in the previous series of patches. But for the moment I will leave this aside anyway. Cheers, Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
