[isabelle-dev] Consolidation of manual naming

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Mon Apr 7 17:21:32 CEST 2014


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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 263 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20140407/b4781e12/attachment.sig>


More information about the isabelle-dev mailing list