>> Nevertheless I still think its a good idea to spend half an hour to >> establish a more strict name correspondance while keeping the >> (lowercase) document names stable, e.g. >> >> foo-bar <-:-> Foo_Bar > > I now see b266e7a86485 with foo-bar <-:-> Foo-Bar. > > It is still unclear to me what the actual confusion was, and what is the > improvement. A "-" within a session name is obsolete for a long time -- > it is in conflict with session-qualified theory names and plain long_id > token syntax. (That is not very relevant for Doc sessions, though.)
When inspecting the ROOT file I saw the session name for »ZF-Logics« and gave that some authority. Maybe it is best if I will move on »ZF_Logics« etc. in yet another iteration to get rid of these historic names. At least that made the confusion apparent. 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