# HG changeset patch
# User wenzelm
# Date 1322395962 -3600
# Node ID 02afa20cf397040c0a3b01d19147b9aafb1f3dae
# Parent  4014bc2a09fff91ddd84d3a009d39aa2db8edf7e
refined "literal" document style, with some correspondence to actual text source;

diff -r 4014bc2a09ff -r 02afa20cf397 doc-src/IsarImplementation/style.sty
--- a/doc-src/IsarImplementation/style.sty	Sun Nov 27 12:52:52 2011 +0100
+++ b/doc-src/IsarImplementation/style.sty	Sun Nov 27 13:12:42 2011 +0100
@@ -64,7 +64,7 @@
 \newcommand{\isasymTHEOREM}{\isakeyword{theorem}}
 \newcommand{\isasymDEFINITION}{\isakeyword{definition}}
 
-\isabellestyle{itunderscore}
+\isabellestyle{literal}
 
 \railtermfont{\isabellestyle{tt}}
 \railnontermfont{\isabellestyle{itunderscore}}
diff -r 4014bc2a09ff -r 02afa20cf397 doc-src/IsarRef/style.sty
--- a/doc-src/IsarRef/style.sty	Sun Nov 27 12:52:52 2011 +0100
+++ b/doc-src/IsarRef/style.sty	Sun Nov 27 13:12:42 2011 +0100
@@ -36,8 +36,8 @@
 
 \parindent 0pt\parskip 0.5ex
 
-\isabellestyle{itunderscore}
+\isabellestyle{literal}
 
 \railtermfont{\isabellestyle{tt}}
-\railnontermfont{\isabellestyle{itunderscore}}
-\railnamefont{\isabellestyle{itunderscore}}
+\railnontermfont{\isabellestyle{literal}}
+\railnamefont{\isabellestyle{literal}}
diff -r 4014bc2a09ff -r 02afa20cf397 lib/texinputs/isabelle.sty
--- a/lib/texinputs/isabelle.sty	Sun Nov 27 12:52:52 2011 +0100
+++ b/lib/texinputs/isabelle.sty	Sun Nov 27 13:12:42 2011 +0100
@@ -194,10 +194,12 @@
 \def\isacharverbatimclose{\isamath{\rangle\!\rangle}}%
 }
 
-\newcommand{\isabellestyleitunderscore}{%
+\newcommand{\isabellestyleliteral}{%
 \isabellestyleit%
 \def\isacharunderscore{\_}%
 \def\isacharunderscorekeyword{\_}%
+\chardef\isacharbackquoteopen=`\`%
+\chardef\isacharbackquoteclose=`\`%
 }
 
 \newcommand{\isabellestylesl}{%