make underscores visually appear as such, although TeX-nically they are just rules (e.g. cannot be searched);

--- a/doc-src/IsarImplementation/style.sty	Sat Jan 16 21:14:15 2010 +0100
+++ b/doc-src/IsarImplementation/style.sty	Thu Jan 28 22:19:27 2010 +0100
@@ -19,7 +19,6 @@
 \pagestyle{headings}
 \sloppy
 \binperiod
-\underscoreon
 
 \renewcommand{\isadigit}[1]{\isamath{#1}}
 
@@ -49,9 +48,7 @@
 \newcommand{\isasymDEFINITION}{\isakeyword{definition}}
 
 \isabellestyle{it}
-
-
-%%% Local Variables: 
-%%% mode: latex
-%%% TeX-master: "implementation"
-%%% End: 
+\underscoreon
+\renewcommand{\isacharunderscore}{\_}
+\renewcommand{\isacharunderscorekeyword}{\_}
+\newcommand{\isasymdash}{\mbox{-}}