keep normal size for %mlref tag;
authorwenzelm
Fri, 08 Oct 2010 21:11:56 +0100
changeset 39828 4303afd3612a
parent 39827 d829ce302ca4
child 39829 f5ea50decd9f
keep normal size for %mlref tag;
doc-src/IsarImplementation/style.sty
--- a/doc-src/IsarImplementation/style.sty	Fri Oct 08 20:59:01 2010 +0100
+++ b/doc-src/IsarImplementation/style.sty	Fri Oct 08 21:11:56 2010 +0100
@@ -26,7 +26,7 @@
 
 \isafoldtag{FIXME}
 \isakeeptag{mlref}
-\renewcommand{\isatagmlref}{\subsection*{\makebox[0pt][r]{\fbox{ML}~~}Reference}\begingroup\def\isastyletext{\rm}\small}
+\renewcommand{\isatagmlref}{\subsection*{\makebox[0pt][r]{\fbox{ML}~~}Reference}\begingroup\def\isastyletext{\rm}}
 \renewcommand{\endisatagmlref}{\endgroup}
 
 \isakeeptag{mlex}