# HG changeset patch
# User nipkow
# Date 1352485307 -3600
# Node ID 20bacff859842e3ae480ae1bca9425958861f5f6
# Parent  6fe18351e9ddfe83f19cf19653cc605363655f52# Parent  e8af1889606092521e1bdb7136699fe718b43b9a
merged

diff -r 6fe18351e9dd -r 20bacff85984 src/HOL/IMP/document/root.tex
--- a/src/HOL/IMP/document/root.tex	Fri Nov 09 14:31:26 2012 +0100
+++ b/src/HOL/IMP/document/root.tex	Fri Nov 09 19:21:47 2012 +0100
@@ -11,6 +11,9 @@
 \urlstyle{rm}
 \isabellestyle{it}
 
+\renewcommand{\isacharunderscore}{\_}
+\renewcommand{\isacharunderscorekeyword}{\_}
+
 % for uniform font size
 \renewcommand{\isastyle}{\isastyleminor}