[isabelle-dev] Consolidation of manual naming

[Tobias Nipkow]

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-dev at in.tum.de 
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>