[isabelle-dev] Consolidation of manual naming

[Makarius]

On Mon, 7 Apr 2014, Florian Haftmann wrote:

>>> 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.

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.

We do have a tradition to get things right eventually, but for that there 
needs to be a clear direction, and some level of significance for a change 
to be considered: it needs 2-3 good reasons, not just half a reason.


 	Makarius