The past days have seen a substantial renovation of the infrastructure for named targets. Highlights:
* 6254c51cd210 – More appropriate treatment of definitions and abbreviations in nested local theories on top of class target. @Andreas This should resolve your issue from https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2014-February/msg00136.html * 56f3351cc492 – Farewell to Named_Target.reinit, an old and odd left-over. * 63c7b29d29ac – This was an attempt to make additional non-canonical interpretations of classes behave more similiar to ordinary locale interpretation esp. wrt. notation syntax. Unfortunately, there are still global interpretations for class order which under these circumstances produce nonsense wrt. to _ < _ and _ <= _ and similar, so this effect had to be reverted in 329f7f76f0a4. It is high time to get rid of these global interpretations of rich type classes. * de00494fa8b3 – Since the very beginning of the class target there has been an »educated guess« to handle constant declarations properly. This is now far less ad-hoc, based on identity of morphisms rather than obscure peek criteria. The identity of morphisms is currently established observing the effect of morphisms on bindings and terms, and this is still some kind of heuristic. Future maybe will yield more elaborate approaches. Btw. there are still scattered ocurences of »query« operations like Named_Target.locale_of etc. which are essentially a violation of the local theory abstraction. But I am optimistic that we can get rid of those in the long run. To get a glimpse how things have evolved over time, see here the state of the art in Isabelle2009-2 (still without nested local theories!) http://isabelle.in.tum.de/repos/isabelle/raw-file/35815ce9218a/src/Pure/Isar/theory_target.ML and now the current polished version http://isabelle.in.tum.de/repos/isabelle/raw-file/4cf607675df8/src/Pure/Isar/generic_target.ML http://isabelle.in.tum.de/repos/isabelle/raw-file/4cf607675df8/src/Pure/Isar/named_target.ML where any obscurity has vanished from named_target.ML (which goes back to the ancient theory_target.ML). 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 isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
