[isabelle] Underscore vs Hyphen in Document Preparation



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{\_}}%

It works, but it I wonder if this is the proper way.

Thanks for any comments on that!
-- 
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
www.inf.pucrs.br/alfio
Lattes:  http://lattes.cnpq.br/4016080665372277
Associate Professor at Faculty of Informatics (PUCRS)
Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática
90619-900 -Porto Alegre - RS - Brasil



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