# HG changeset patch
# User haftmann
# Date 1228728460 -3600
# Node ID 9a1eaad4a7bb3d3d294adc85ff273a97257718a4
# Parent  31110b40eae76e5f5048afb6c7fee71b6f4e0315
tuned LaTeX files

diff -r 31110b40eae7 -r 9a1eaad4a7bb doc-src/IsarAdvanced/Codegen/codegen.tex
--- a/doc-src/IsarAdvanced/Codegen/codegen.tex	Mon Dec 08 10:14:50 2008 +0100
+++ b/doc-src/IsarAdvanced/Codegen/codegen.tex	Mon Dec 08 10:27:40 2008 +0100
@@ -1,5 +1,3 @@
-
-%% $Id$
 
 \documentclass[12pt,a4paper,fleqn]{report}
 \usepackage{latexsym,graphicx}
@@ -12,43 +10,10 @@
 \usepackage{tikz}
 \usepackage{../../pdfsetup}
 
-%% setup
-
-% hyphenation
 \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{\isatypewriter}{\fontsize{9pt}{0pt}\tt\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{9pt}}
-
-% 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}
-
-% hack
-\newcommand{\isasymSML}{SML}
-
-
-%% contents
-
 \title{\includegraphics[scale=0.5]{isabelle_isar}
   \\[4ex] Code generation from Isabelle/HOL theories}
 \author{\emph{Florian Haftmann}}
@@ -75,7 +40,6 @@
 \input{Thy/document/ML.tex}
 
 \begingroup
-%\tocentry{\bibname}
 \bibliographystyle{plain} \small\raggedright\frenchspacing
 \bibliography{../../manual}
 \endgroup
diff -r 31110b40eae7 -r 9a1eaad4a7bb doc-src/IsarAdvanced/Codegen/style.sty
--- a/doc-src/IsarAdvanced/Codegen/style.sty	Mon Dec 08 10:14:50 2008 +0100
+++ b/doc-src/IsarAdvanced/Codegen/style.sty	Mon Dec 08 10:27:40 2008 +0100
@@ -1,5 +1,3 @@
-
-%% $Id$
 
 %% toc
 \newcommand{\tocentry}[1]{\cleardoublepage\phantomsection\addcontentsline{toc}{chapter}{#1}
@@ -7,15 +5,6 @@
 
 %% references
 \newcommand{\secref}[1]{\S\ref{#1}}
-\newcommand{\chref}[1]{chapter~\ref{#1}}
-\newcommand{\figref}[1]{figure~\ref{#1}}
-
-%% glossary
-\renewcommand{\glossary}[2]{\nomenclature{\bf #1}{#2}}
-\newcommand{\seeglossary}[1]{\emph{#1}}
-\newcommand{\glossaryname}{Glossary}
-\renewcommand{\nomname}{\glossaryname}
-\renewcommand{\pagedeclaration}[1]{\nobreak\quad\dotfill~page~\bold{#1}}
 
 %% index
 \newcommand{\indexml}[1]{\index{\emph{#1}|bold}}
@@ -23,38 +12,49 @@
 \newcommand{\indexmlstructure}[1]{\index{\emph{#1} (structure)|bold}}
 \newcommand{\indexmlfunctor}[1]{\index{\emph{#1} (functor)|bold}}
 
-%% math
-\newcommand{\text}[1]{\mbox{#1}}
-\newcommand{\isasymvartheta}{\isamath{\theta}}
-\newcommand{\isactrlvec}[1]{\emph{$\overline{#1}$}}
+%% logical markup
+\newcommand{\strong}[1]{{\bfseries {#1}}}
+\newcommand{\qn}[1]{\emph{#1}}
+
+%% typographic conventions
+\newcommand{\qt}[1]{``{#1}''}
+
+%% verbatim text
+\newcommand{\isatypewriter}{\fontsize{9pt}{0pt}\tt\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{9pt}}
 
+%% 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}
+
+%% a trick
+\newcommand{\isasymSML}{SML}
+
+%% presentation
 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
 
 \pagestyle{headings}
-\sloppy
 \binperiod
 \underscoreon
 
 \renewcommand{\isadigit}[1]{\isamath{#1}}
 
+%% ml reference
 \newenvironment{mldecls}{\par\noindent\begingroup\footnotesize\def\isanewline{\\}\begin{tabular}{l}}{\end{tabular}\smallskip\endgroup}
 
-\isafoldtag{FIXME}
 \isakeeptag{mlref}
 \renewcommand{\isatagmlref}{\subsection*{\makebox[0pt][r]{\fbox{\ML}~~}Reference}\begingroup\def\isastyletext{\rm}\small}
 \renewcommand{\endisatagmlref}{\endgroup}
 
-\newcommand{\isasymGUESS}{\isakeyword{guess}}
-\newcommand{\isasymOBTAIN}{\isakeyword{obtain}}
-\newcommand{\isasymTHEORY}{\isakeyword{theory}}
-\newcommand{\isasymUSES}{\isakeyword{uses}}
-\newcommand{\isasymEND}{\isakeyword{end}}
-\newcommand{\isasymCONSTS}{\isakeyword{consts}}
-\newcommand{\isasymDEFS}{\isakeyword{defs}}
-\newcommand{\isasymTHEOREM}{\isakeyword{theorem}}
-\newcommand{\isasymDEFINITION}{\isakeyword{definition}}
+\isabellestyle{it}
 
-\isabellestyle{it}
 
 %%% Local Variables: 
 %%% mode: latex