Re: [isabelle] Underscore vs Hyphen in Document Preparation

Am 02/12/2013 05:04, schrieb Alfio Martini:
> Dear Isabelle Users,
> Documents generated with Isabelle build tool
> produce an hyphen instead of an underscore whenever the
> later is used in identifiers and concrete syntax annotation.
> I think this is (a bit) unfortunate as a  choice for a default definition.
> After a brief inspection of the isabelle.sty file, I added the
> following workaround to my prelude.tex file:
> def\isacharunderscore{\mbox{\_}}%

For tutorials, where every character matters, I do (more or less) exactly that
and it works fine. In standard papers I quite like the "-".


> It works, but it I wonder if this is the proper way.
> Thanks for any comments on that!

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.