1.1 --- a/doc-src/IsarImplementation/style.sty	Thu Jan 28 22:39:48 2010 +0100
     1.2 +++ b/doc-src/IsarImplementation/style.sty	Fri Jan 29 23:57:57 2010 +0100
     1.3 @@ -29,6 +29,13 @@
     1.4  \renewcommand{\isatagmlref}{\subsection*{\makebox[0pt][r]{\fbox{\ML}~~}Reference}\begingroup\def\isastyletext{\rm}\small}
     1.5  \renewcommand{\endisatagmlref}{\endgroup}
     1.6  
     1.7 +\isakeeptag{mlex}
     1.8 +\renewcommand{\isatagmlex}{\subsection*{\makebox[0pt][r]{\fbox{\ML}~~}Examples}}
     1.9 +\renewcommand{\endisatagmlex}{}
    1.10 +
    1.11 +\renewcommand{\isatagML}{\begingroup\isabellestyle{default}\isastyle\def\isadigit##1{##1}}
    1.12 +\renewcommand{\endisatagML}{\endgroup}
    1.13 +
    1.14  \newcommand{\minorcmd}[1]{{\sf #1}}
    1.15  \newcommand{\isasymtype}{\minorcmd{type}}
    1.16  \newcommand{\isasymval}{\minorcmd{val}}