# HG changeset patch # User wenzelm # Date 1209761278 -7200 # Node ID 06d6b1242dcfa9b0f9ad6cca8314f1c8d999b121 # Parent e258050a30764b0f10e2b13cfdac829253e29c95 use underscore for underscore; diff -r e258050a3076 -r 06d6b1242dcf doc-src/IsarRef/style.sty --- a/doc-src/IsarRef/style.sty Fri May 02 22:47:23 2008 +0200 +++ b/doc-src/IsarRef/style.sty Fri May 02 22:47:58 2008 +0200 @@ -44,6 +44,8 @@ \newcommand{\isasymDEFINITION}{\isakeyword{definition}} \isabellestyle{it} +\renewcommand{\isacharunderscore}{\_} +\renewcommand{\isacharunderscorekeyword}{\_} %%% Local Variables: %%% mode: latex