--- a/doc-src/IsarAdvanced/Codegen/codegen.tex Fri Oct 10 06:49:44 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/codegen.tex Fri Oct 10 15:23:33 2008 +0200
@@ -11,39 +11,44 @@
\usepackage{tikz}
\usepackage{../../pdfsetup}
-\newcommand{\isaverbatim}{\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{8pt}\fontsize{8pt}{0pt}}
-
-\makeatletter
-
-\isakeeptag{quoteme}
-\newenvironment{quoteme}{\begin{quote}\isa@parindent\parindent\parindent0pt\isa@parskip\parskip\parskip0pt}{\end{quote}}
-\renewcommand{\isatagquoteme}{\begin{quoteme}}
-\renewcommand{\endisatagquoteme}{\end{quoteme}}
+%% setup
-\isakeeptag{tt}
-\renewcommand{\isatagtt}{\begin{quoteme}\isabellestyle{tt}\isastyle}
-\renewcommand{\endisatagtt}{\end{quoteme}\isabellestyle{it}\isastyle}
-
-\makeatother
-
-\newcommand{\isactrlbvec}{\emph\bgroup\begin{math}{}\overline\bgroup\mbox\bgroup\isastylescript}
-\newcommand{\isactrlevec}{\egroup\egroup\end{math}\egroup}
-
-\newcommand{\qt}[1]{``#1''}
-\newcommand{\qtt}[1]{"{}{#1}"{}}
-\newcommand{\qn}[1]{\emph{#1}}
-\newcommand{\strong}[1]{{\bfseries #1}}
-\newcommand{\fixme}[1][!]{\strong{FIXME: #1}}
-
+% configuration
\hyphenation{Isabelle}
\hyphenation{Isar}
+% logical markup
+\newcommand{\strong}[1]{{\bfseries {#1}}}
+\newcommand{\qn}[1]{\emph{#1}}
+
+% typographic conventions
+\newcommand{\qt}[1]{``{#1}''}
+
+% verbatim text
+\newcommand{\isaverbatim}{\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{8pt}\fontsize{8pt}{0pt}}
+
+% invisibility
\isadroptag{theory}
+
+% quoted segments
+\makeatletter
+\isakeeptag{quote}
+\newenvironment{quotesegment}{\begin{quote}\isa@parindent\parindent\parindent0pt\isa@parskip\parskip\parskip0pt}{\end{quote}}
+\renewcommand{\isatagquote}{\begin{quotesegment}}
+\renewcommand{\endisatagquote}{\end{quotesegment}}
+\makeatother
+
+\isakeeptag{quotett}
+\renewcommand{\isatagquotett}{\begin{quotesegment}\isabellestyle{tt}\isastyle}
+\renewcommand{\endisatagquotett}{\end{quotesegment}\isabellestyle{it}\isastyle}
+
+
+%% contents
+
\title{\includegraphics[scale=0.5]{isabelle_isar}
\\[4ex] Code generation from Isabelle/HOL theories}
\author{\emph{Florian Haftmann}}
-
\begin{document}
\maketitle