# HG changeset patch
# User wenzelm
# Date 1334843252 -7200
# Node ID 3b89d59a944b75475e24db052269c2c80c357049
# Parent  6eb3b3ae4ccbb3c6fef6390d46ad3e992866aba4
accomodate digits within Isar command names, notably 'try0';

diff -r 6eb3b3ae4ccb -r 3b89d59a944b doc-src/IsarRef/style.sty
--- a/doc-src/IsarRef/style.sty	Thu Apr 19 15:02:13 2012 +0200
+++ b/doc-src/IsarRef/style.sty	Thu Apr 19 15:47:32 2012 +0200
@@ -13,16 +13,18 @@
 \newcommand{\figref}[1]{figure~\ref{#1}}
 \newcommand{\Figref}[1]{Figure~\ref{#1}}
 
+%% Isar
+\newcommand{\isasymBBAR}{{\,\newdimen{\tmpheight}\settoheight\tmpheight{\isacharbar}\rule{1pt}{\tmpheight}\,}}
+\isafoldtag{noproof}\def\isafoldnoproof{~\isafold{proof}}
+\newcommand{\isadigitreset}{\def\isadigit##1{##1}}
+\renewcommand{\isacommand}[1]{\isakeyword{\isadigitreset#1}}
+
 %% ML
 \newenvironment{mldecls}{\par\noindent\begingroup\def\isanewline{\\}\begin{tabular}{ll}}{\end{tabular}\medskip\endgroup}
 
-\renewcommand{\isatagML}{\begingroup\isabellestyle{default}\isastyle\def\isadigit##1{##1}}
+\renewcommand{\isatagML}{\begingroup\isabellestyle{default}\isastyle\isadigitreset}
 \renewcommand{\endisatagML}{\endgroup}
 
-%% Isar
-\newcommand{\isasymBBAR}{{\,\newdimen{\tmpheight}\settoheight\tmpheight{\isacharbar}\rule{1pt}{\tmpheight}\,}}
-\isafoldtag{noproof}\def\isafoldnoproof{~\isafold{proof}}
-
 %% math
 \newcommand{\isasymstrut}{\isamath{\mathstrut}}
 \newcommand{\isasymvartheta}{\isamath{\,\theta}}