CookBook/document/root.tex
changeset 106 bdd82350cf22
parent 101 123401a5c8e9
child 108 8bea3f74889d
equal deleted inserted replaced
105:f49dc7e96235 106:bdd82350cf22
    76 \newenvironment{vanishML}{%
    76 \newenvironment{vanishML}{%
    77 \renewcommand{\isacommand}[1]{}%
    77 \renewcommand{\isacommand}[1]{}%
    78 \renewcommand{\isacharverbatimopen}{}%
    78 \renewcommand{\isacharverbatimopen}{}%
    79 \renewcommand{\isacharverbatimclose}{}}{}
    79 \renewcommand{\isacharverbatimclose}{}}{}
    80 
    80 
    81 \isakeeptag{CookBookML}
    81 \isakeeptag{TutorialML}
    82 \renewcommand{\isatagCookBookML}{\begin{vanishML}\begin{graybox}}
    82 \renewcommand{\isatagTutorialML}{\begin{vanishML}\begin{graybox}}
    83 \renewcommand{\endisatagCookBookML}{\end{graybox}\end{vanishML}}
    83 \renewcommand{\endisatagTutorialML}{\end{graybox}\end{vanishML}}
    84 
    84 
    85 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    85 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    86 % for code that has line numbers
    86 % for code that has line numbers
    87 \isakeeptag{linenumbers}
    87 \isakeeptag{linenumbers}
    88 \renewcommand{\isataglinenumbers}{\begin{vanishML}\begin{graybox}\resetlinenumber\internallinenumbers}
    88 \renewcommand{\isataglinenumbers}{\begin{vanishML}\begin{graybox}\resetlinenumber\internallinenumbers}
   101 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   101 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   102 \begin{document}
   102 \begin{document}
   103 
   103 
   104 \title{\mbox{}\\[-10ex]
   104 \title{\mbox{}\\[-10ex]
   105        \includegraphics[scale=0.5]{cookbook-logo.jpg}\\[3ex]
   105        \includegraphics[scale=0.5]{cookbook-logo.jpg}\\[3ex]
   106        The Isabelle Programmer's Cookbook (fragment)}
   106        The Isabelle Programming Tutorial (fragment)}
   107 
   107 
   108 \author{with contributions by:\\[2ex] 
   108 \author{with contributions by:\\[2ex] 
   109         \begin{tabular}{r@{\hspace{1.8mm}}l}
   109         \begin{tabular}{r@{\hspace{1.8mm}}l}
   110         Stefan & Berghofer\\
   110         Stefan & Berghofer\\
   111         Sascha & Böhme\\
   111         Sascha & Böhme\\