doc-src/IsarAdvanced/Codegen/codegen.tex
changeset 28428 fd007794561f
parent 28419 f65e8b318581
child 28447 df77ed974a78
equal deleted inserted replaced
28427:cc9f7d99fb73 28428:fd007794561f
     8 \usepackage{../../iman,../../extra,../../isar,../../proof}
     8 \usepackage{../../iman,../../extra,../../isar,../../proof}
     9 \usepackage{../../isabelle,../../isabellesym}
     9 \usepackage{../../isabelle,../../isabellesym}
    10 \usepackage{style}
    10 \usepackage{style}
    11 \usepackage{../../pdfsetup}
    11 \usepackage{../../pdfsetup}
    12 
    12 
       
    13 \newcommand{\isaverbatim}{\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{8pt}\fontsize{8pt}{0pt}}
       
    14 
    13 \makeatletter
    15 \makeatletter
    14 
    16 
    15 \newcommand{\isaverbatim}{\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{8pt}\fontsize{8pt}{0pt}}
       
    16 \isakeeptag{quoteme}
    17 \isakeeptag{quoteme}
    17 \newenvironment{quoteme}{\begin{quote}\isa@parindent\parindent\parindent0pt\isa@parskip\parskip\parskip0pt}{\end{quote}}
    18 \newenvironment{quoteme}{\begin{quote}\isa@parindent\parindent\parindent0pt\isa@parskip\parskip\parskip0pt}{\end{quote}}
    18 \renewcommand{\isatagquoteme}{\begin{quoteme}}
    19 \renewcommand{\isatagquoteme}{\begin{quoteme}}
    19 \renewcommand{\endisatagquoteme}{\end{quoteme}}
    20 \renewcommand{\endisatagquoteme}{\end{quoteme}}
    20 
    21 
       
    22 \isakeeptag{tt}
       
    23 \renewcommand{\isatagtt}{\begin{quoteme}\isabellestyle{tt}\isastyle}
       
    24 \renewcommand{\endisatagtt}{\end{quoteme}\isabellestyle{it}\isastyle}
       
    25 
    21 \makeatother
    26 \makeatother
    22 
    27 
    23 \isakeeptag{tt}
    28 \newcommand{\isactrlbvec}{\emph\bgroup\begin{math}{}\overline\bgroup\mbox\bgroup\isastylescript}
    24 \renewcommand{\isatagtt}{\isabellestyle{tt}\isastyle}
    29 \newcommand{\isactrlevec}{\egroup\egroup\end{math}\egroup}
    25 \renewcommand{\endisatagtt}{\isabellestyle{it}\isastyle}
       
    26 
    30 
    27 \newcommand{\qt}[1]{``#1''}
    31 \newcommand{\qt}[1]{``#1''}
    28 \newcommand{\qtt}[1]{"{}{#1}"{}}
    32 \newcommand{\qtt}[1]{"{}{#1}"{}}
    29 \newcommand{\qn}[1]{\emph{#1}}
    33 \newcommand{\qn}[1]{\emph{#1}}
    30 \newcommand{\strong}[1]{{\bfseries #1}}
    34 \newcommand{\strong}[1]{{\bfseries #1}}