refined "literal" document style, with some correspondence to actual text source;

--- 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}}

--- 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}}

--- 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}{%