# HG changeset patch # User wenzelm # Date 1420918133 -3600 # Node ID 43281cd62cb00280d65399bbc617449348aaae25 # Parent fd9102b419f525a3bfc64ef93f303ddd6922f59b tuned latex; diff -r fd9102b419f5 -r 43281cd62cb0 src/Doc/isar.sty --- a/src/Doc/isar.sty Sat Jan 10 16:35:21 2015 +0100 +++ b/src/Doc/isar.sty Sat Jan 10 20:28:53 2015 +0100 @@ -4,8 +4,8 @@ {\ifthenelse{\equal{}{#1}}{\index{#3 (#2)|bold}}{\index{#3 (#1\ #2)|bold}}} \newcommand{\indexref}[3]{\ifthenelse{\equal{}{#1}}{\index{#3 (#2)}}{\index{#3 (#1\ #2)}}} -\newcommand{\isasystem}[1]{{\def\isacharminus{-}\def\isacharunderscore{\_}\tt #1}} -\newcommand{\isatool}[1]{{\def\isacharminus{-}\def\isacharunderscore{\_}\tt isabelle #1}} +\newcommand{\isasystem}[1]{{\def\isacharminus{-}\def\isacharunderscore{\_}\isadigitreset\tt #1}} +\newcommand{\isatool}[1]{{\def\isacharminus{-}\def\isacharunderscore{\_}\isadigitreset\tt isabelle #1}} \newcommand{\indexoutertoken}[1]{\indexdef{}{syntax}{#1}} \newcommand{\indexouternonterm}[1]{\indexdef{}{syntax}{#1}}