tag ML as in IsarImplementation;
authorwenzelm
Tue, 03 May 2011 15:37:17 +0200
changeset 43525b1a051891ec4
parent 43524 d25bf6996368
child 43526 eb95e2f3b218
tag ML as in IsarImplementation;
doc-src/IsarRef/style.sty
     1.1 --- a/doc-src/IsarRef/style.sty	Tue May 03 15:35:07 2011 +0200
     1.2 +++ b/doc-src/IsarRef/style.sty	Tue May 03 15:37:17 2011 +0200
     1.3 @@ -16,6 +16,9 @@
     1.4  %% ML
     1.5  \newenvironment{mldecls}{\par\noindent\begingroup\def\isanewline{\\}\begin{tabular}{ll}}{\end{tabular}\medskip\endgroup}
     1.6  
     1.7 +\renewcommand{\isatagML}{\begingroup\isabellestyle{default}\isastyle\def\isadigit##1{##1}}
     1.8 +\renewcommand{\endisatagML}{\endgroup}
     1.9 +
    1.10  %% Isar
    1.11  \newcommand{\isasymBBAR}{{\,\newdimen{\tmpheight}\settoheight\tmpheight{\isacharbar}\rule{1pt}{\tmpheight}\,}}
    1.12  \isafoldtag{noproof}\def\isafoldnoproof{~\isafold{proof}}
    1.13 @@ -42,4 +45,4 @@
    1.14  \def\rail@termfont{\isabellestyle{tt}\setupunderscore}
    1.15  \def\rail@nontfont{\isabellestyle{it}\setupunderscore}
    1.16  \def\rail@namefont{\isabellestyle{it}\setupunderscore}
    1.17 -\makeatother
    1.18 \ No newline at end of file
    1.19 +\makeatother