> context B begin > interpretation A > interpretation A' > interpretation A'' > end > sublocale B < A''
What you currently have in many places (e.g. http://isabelle.in.tum.de/reports/Isabelle/file/757fa47af981/src/HOL/Lattices.thy) is the pattern. context B begin … end sublocale B < … context B begin … end sublocale B < … context B begin … end When giving up the paradigm that sublocale dependencies may only be introduced on the global level, youo end up with sth like context B begin … intepretation … … intepretation … … end which is compacter and more intuitive. 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
