--- 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
--- 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