| changeset 28714 | 1992553cccfe |
| parent 28565 | 519b17118926 |
| child 28727 | 185110a4b97a |
--- a/doc-src/IsarAdvanced/Classes/classes.tex Fri Oct 31 10:39:04 2008 +0100 +++ b/doc-src/IsarAdvanced/Classes/classes.tex Mon Nov 03 14:15:25 2008 +0100 @@ -24,7 +24,7 @@ \newcommand{\qt}[1]{``{#1}''} % verbatim text -\newcommand{\isaverbatim}{\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{8pt}\fontsize{8pt}{0pt}} +\newcommand{\isaverbatim}{\fontsize{9pt}{0pt}\tt\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{9pt}} % invisibility \isadroptag{theory}