# HG changeset patch
# User wenzelm
# Date 1264805877 -3600
# Node ID e59915c6a552ba2526106e9820dad0dc40446026
# Parent  e35f608f81a2e5531c2c434cddf2d055a29e1eb2
basic setup for ML examples: tag "mlex";

diff -r e35f608f81a2 -r e59915c6a552 doc-src/IsarImplementation/style.sty
--- a/doc-src/IsarImplementation/style.sty	Thu Jan 28 22:39:48 2010 +0100
+++ b/doc-src/IsarImplementation/style.sty	Fri Jan 29 23:57:57 2010 +0100
@@ -29,6 +29,13 @@
 \renewcommand{\isatagmlref}{\subsection*{\makebox[0pt][r]{\fbox{\ML}~~}Reference}\begingroup\def\isastyletext{\rm}\small}
 \renewcommand{\endisatagmlref}{\endgroup}
 
+\isakeeptag{mlex}
+\renewcommand{\isatagmlex}{\subsection*{\makebox[0pt][r]{\fbox{\ML}~~}Examples}}
+\renewcommand{\endisatagmlex}{}
+
+\renewcommand{\isatagML}{\begingroup\isabellestyle{default}\isastyle\def\isadigit##1{##1}}
+\renewcommand{\endisatagML}{\endgroup}
+
 \newcommand{\minorcmd}[1]{{\sf #1}}
 \newcommand{\isasymtype}{\minorcmd{type}}
 \newcommand{\isasymval}{\minorcmd{val}}