I consider this twofold renaming of directories pointless, and as you know, it required a twofold update in some other theories of mine. I guess I should have stated my displeasure earlier but thought that since Makarius had already stated he didn't even see the problem, this would discourage you. Obviously I underestimated you ;-)
Nuff said. Tobias On 11/04/2014 15:54, Florian Haftmann wrote: >>> 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. >> >> I still don't understand what the confusion actually is. These things >> are really old, especially the "logics" manuals, which used to be just >> one latex document a long time ago. It is not always possible to have >> immediately obvious canonical names for everything -- there are often >> conflicting side-conditions etc. > > Being in the role of an occasional bypasser in src/Doc, the lack of any > apparent »standard scheme« to glimpse from produces more diversion over > time. E.g. I myself attributed some official status to the session name > »ZF-Logics« which was just an historical accident. You might call this an > instance of the broken-window syndrome. > > Florian > > > > _______________________________________________ isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev