accomodate digits within Isar command names, notably 'try0';
authorwenzelm
Thu, 19 Apr 2012 15:47:32 +0200
changeset 47586 3b89d59a944b
parent 47585 6eb3b3ae4ccb
child 47587 0692eea09cb7
accomodate digits within Isar command names, notably 'try0';
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}}