Hi Christian, > to me the liberal flag seems rather ad-hoc. Wouldn't a proper > hierarchical naming solve this problem (maybe by introducing an > automatic "sub-module" Internal/Auto/Whatever for any theory T, such > that automatic names may be referred to by using > T.Whatever.automatic_name).
we *have* already the concept of binding prefices (what you refer to
here as hierarchical naming), although the theory name part of the
prefix currently is always a singleton. What I have to address is that
you cannot be sure that a given name is already used, regardless how
many prefices you add.
Cheers,
Florian
--
Home:
http://www.in.tum.de/~haftmann
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
