# HG changeset patch
# User haftmann
# Date 1229331524 -3600
# Node ID a5ac0bc68e2bbe98e989c16fbe1147b0b13b1389
# Parent  e2fdd4ce541b050ecf892e0ae0f8bf87766ad2e7
\underscoreoff is now default

diff -r e2fdd4ce541b -r a5ac0bc68e2b doc-src/IsarAdvanced/Classes/style.sty
--- a/doc-src/IsarAdvanced/Classes/style.sty	Mon Dec 15 07:41:07 2008 +0000
+++ b/doc-src/IsarAdvanced/Classes/style.sty	Mon Dec 15 09:58:44 2008 +0100
@@ -30,7 +30,7 @@
 
 \pagestyle{headings}
 \binperiod
-\underscoreon
+\underscoreoff
 
 \renewcommand{\isadigit}[1]{\isamath{#1}}
 
diff -r e2fdd4ce541b -r a5ac0bc68e2b doc-src/IsarAdvanced/Codegen/style.sty
--- a/doc-src/IsarAdvanced/Codegen/style.sty	Mon Dec 15 07:41:07 2008 +0000
+++ b/doc-src/IsarAdvanced/Codegen/style.sty	Mon Dec 15 09:58:44 2008 +0100
@@ -42,7 +42,7 @@
 
 \pagestyle{headings}
 \binperiod
-\underscoreon
+\underscoreoff
 
 \renewcommand{\isadigit}[1]{\isamath{#1}}