# HG changeset patch
# User wenzelm
# Date 1264713567 -3600
# Node ID 3343670206ebfa160e8c8ed9e24faa59c70a8789
# Parent  a5407aabacfef3966ffc51e52c5547cbc52099a1
make underscores visually appear as such, although TeX-nically they are just rules (e.g. cannot be searched);

diff -r a5407aabacfe -r 3343670206eb doc-src/IsarImplementation/style.sty
--- 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{-}}