| changeset 30120 | aaa4667285c8 |
| parent 29733 | f38ccabb2edc |
| child 30242 | aea5d7fa7ef5 |
--- a/doc-src/IsarRef/style.sty Thu Feb 26 20:41:28 2009 +0100 +++ b/doc-src/IsarRef/style.sty Thu Feb 26 20:44:07 2009 +0100 @@ -15,7 +15,6 @@ %% ML \newenvironment{mldecls}{\par\noindent\begingroup\def\isanewline{\\}\begin{tabular}{ll}}{\end{tabular}\medskip\endgroup} -\newcommand{\indexml}[1]{\index{#1 (ML value)|bold}} %% Isar \newcommand{\isasymBBAR}{{\,\newdimen{\tmpheight}\settoheight\tmpheight{\isacharbar}\rule{1pt}{\tmpheight}\,}}