| changeset 28727 | 185110a4b97a |
| parent 28714 | 1992553cccfe |
| child 29017 | 9a1eaad4a7bb |
--- a/doc-src/IsarAdvanced/Codegen/codegen.tex Mon Nov 10 08:18:58 2008 +0100 +++ b/doc-src/IsarAdvanced/Codegen/codegen.tex Mon Nov 10 09:03:28 2008 +0100 @@ -26,7 +26,7 @@ \newcommand{\qt}[1]{``{#1}''} % verbatim text -\newcommand{\isaverbatim}{\fontsize{9pt}{0pt}\tt\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{9pt}} +\newcommand{\isatypewriter}{\fontsize{9pt}{0pt}\tt\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{9pt}} % invisibility \isadroptag{theory}