diff -r a9fa81e150c9 -r b3baeeabfe0b src/Doc/Main/document/root.tex
--- a/src/Doc/Main/document/root.tex	Thu Aug 14 12:33:21 2014 +0200
+++ b/src/Doc/Main/document/root.tex	Thu Aug 14 12:46:37 2014 +0200
@@ -15,17 +15,15 @@
 % this should be the last package used
 \usepackage{pdfsetup}
 
-% urls in roman style, theory text in math-similar italics
+% urls in roman style, theory text in math-similar italics, with literal underscore
 \urlstyle{rm}
-\isabellestyle{it}
+\isabellestyle{literal}
 
 % for uniform font size
 \renewcommand{\isastyle}{\isastyleminor}
 
 \parindent 0pt\parskip 0.5ex
 
-\renewcommand{\isacharunderscore}{\_}
-
 \usepackage{supertabular}
 
 \begin{document}