CookBook/document/root.tex
changeset 115 039845fc96bd
parent 114 13fd0a83d3c3
child 116 c9ff326e3ce5
equal deleted inserted replaced
114:13fd0a83d3c3 115:039845fc96bd
    91 % should only be used in ML code
    91 % should only be used in ML code
    92 \isakeeptag{linenosgray}
    92 \isakeeptag{linenosgray}
    93 \renewcommand{\isataglinenosgray}{\begin{vanishML}\begin{graybox}\resetlinenumber\internallinenumbers}
    93 \renewcommand{\isataglinenosgray}{\begin{vanishML}\begin{graybox}\resetlinenumber\internallinenumbers}
    94 \renewcommand{\endisataglinenosgray}{\par\nolinenumbers\end{graybox}\end{vanishML}}
    94 \renewcommand{\endisataglinenosgray}{\par\nolinenumbers\end{graybox}\end{vanishML}}
    95 
    95 
       
    96 \isakeeptag{small}
       
    97 \renewcommand{\isatagsmall}{\begingroup\small}
       
    98 \renewcommand{\endisatagsmall}{\endgroup}
       
    99 
    96 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   100 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    97 \renewenvironment{isabelle}
   101 \renewenvironment{isabelle}
    98 {\begin{trivlist}\begin{isabellebody}\small\item\relax}
   102 {\begin{trivlist}\begin{isabellebody}\small\item\relax}
    99 {\end{isabellebody}\end{trivlist}}
   103 {\end{isabellebody}\end{trivlist}}
   100 
   104