fixed underscores
authornipkow
Fri, 09 Nov 2012 19:16:31 +0100
changeset 50043 e8af18896060
parent 50029 31c9294eebe6
child 50044 20bacff85984
fixed underscores
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}