# HG changeset patch # User nipkow # Date 1352484991 -3600 # Node ID e8af1889606092521e1bdb7136699fe718b43b9a # Parent 31c9294eebe6d633a96f1b3677569185859b73c3 fixed underscores diff -r 31c9294eebe6 -r e8af18896060 src/HOL/IMP/document/root.tex --- a/src/HOL/IMP/document/root.tex Thu Nov 08 11:59:50 2012 +0100 +++ b/src/HOL/IMP/document/root.tex Fri Nov 09 19:16:31 2012 +0100 @@ -11,6 +11,9 @@ \urlstyle{rm} \isabellestyle{it} +\renewcommand{\isacharunderscore}{\_} +\renewcommand{\isacharunderscorekeyword}{\_} + % for uniform font size \renewcommand{\isastyle}{\isastyleminor}