[isabelle-dev] Consolidation of manual naming
nipkow at in.tum.de
Fri Apr 11 16:12:19 CEST 2014
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 ;-)
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.
> _______________________________________________ isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev