doc-src/IsarAdvanced/Classes/classes.tex
changeset 28727 185110a4b97a
parent 28714 1992553cccfe
child 29016 31110b40eae7
equal deleted inserted replaced
28726:47ff45771f2c 28727:185110a4b97a
    22 
    22 
    23 % typographic conventions
    23 % typographic conventions
    24 \newcommand{\qt}[1]{``{#1}''}
    24 \newcommand{\qt}[1]{``{#1}''}
    25 
    25 
    26 % verbatim text
    26 % verbatim text
    27 \newcommand{\isaverbatim}{\fontsize{9pt}{0pt}\tt\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{9pt}}
    27 \newcommand{\isatypewriter}{\fontsize{9pt}{0pt}\tt\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{9pt}}
    28 
    28 
    29 % invisibility
    29 % invisibility
    30 \isadroptag{theory}
    30 \isadroptag{theory}
    31 
    31 
    32 % quoted segments
    32 % quoted segments