# HG changeset patch
# User wenzelm
# Date 1304429837 -7200
# Node ID b1a051891ec4e82e78e5173cc5349abf36ee5a4f
# Parent  d25bf6996368264b44de749b0eee96a8dbf0913c
tag ML as in IsarImplementation;

diff -r d25bf6996368 -r b1a051891ec4 doc-src/IsarRef/style.sty
--- a/doc-src/IsarRef/style.sty	Tue May 03 15:35:07 2011 +0200
+++ b/doc-src/IsarRef/style.sty	Tue May 03 15:37:17 2011 +0200
@@ -16,6 +16,9 @@
 %% 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{\endisatagML}{\endgroup}
+
 %% Isar
 \newcommand{\isasymBBAR}{{\,\newdimen{\tmpheight}\settoheight\tmpheight{\isacharbar}\rule{1pt}{\tmpheight}\,}}
 \isafoldtag{noproof}\def\isafoldnoproof{~\isafold{proof}}
@@ -42,4 +45,4 @@
 \def\rail@termfont{\isabellestyle{tt}\setupunderscore}
 \def\rail@nontfont{\isabellestyle{it}\setupunderscore}
 \def\rail@namefont{\isabellestyle{it}\setupunderscore}
-\makeatother
\ No newline at end of file
+\makeatother