tuned LaTeX files
authorhaftmann
Mon Dec 08 10:27:40 2008 +0100 (2008-12-08)
changeset 290179a1eaad4a7bb
parent 29016 31110b40eae7
child 29020 3e95d28114a1
tuned LaTeX files
doc-src/IsarAdvanced/Codegen/codegen.tex
doc-src/IsarAdvanced/Codegen/style.sty
     1.1 --- a/doc-src/IsarAdvanced/Codegen/codegen.tex	Mon Dec 08 10:14:50 2008 +0100
     1.2 +++ b/doc-src/IsarAdvanced/Codegen/codegen.tex	Mon Dec 08 10:27:40 2008 +0100
     1.3 @@ -1,5 +1,3 @@
     1.4 -
     1.5 -%% $Id$
     1.6  
     1.7  \documentclass[12pt,a4paper,fleqn]{report}
     1.8  \usepackage{latexsym,graphicx}
     1.9 @@ -12,43 +10,10 @@
    1.10  \usepackage{tikz}
    1.11  \usepackage{../../pdfsetup}
    1.12  
    1.13 -%% setup
    1.14 -
    1.15 -% hyphenation
    1.16  \hyphenation{Isabelle}
    1.17  \hyphenation{Isar}
    1.18 -
    1.19 -% logical markup
    1.20 -\newcommand{\strong}[1]{{\bfseries {#1}}}
    1.21 -\newcommand{\qn}[1]{\emph{#1}}
    1.22 -
    1.23 -% typographic conventions
    1.24 -\newcommand{\qt}[1]{``{#1}''}
    1.25 -
    1.26 -% verbatim text
    1.27 -\newcommand{\isatypewriter}{\fontsize{9pt}{0pt}\tt\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{9pt}}
    1.28 -
    1.29 -% invisibility
    1.30  \isadroptag{theory}
    1.31  
    1.32 -% quoted segments
    1.33 -\makeatletter
    1.34 -\isakeeptag{quote}
    1.35 -\newenvironment{quotesegment}{\begin{quote}\isa@parindent\parindent\parindent0pt\isa@parskip\parskip\parskip0pt}{\end{quote}}
    1.36 -\renewcommand{\isatagquote}{\begin{quotesegment}}
    1.37 -\renewcommand{\endisatagquote}{\end{quotesegment}}
    1.38 -\makeatother
    1.39 -
    1.40 -\isakeeptag{quotett}
    1.41 -\renewcommand{\isatagquotett}{\begin{quotesegment}\isabellestyle{tt}\isastyle}
    1.42 -\renewcommand{\endisatagquotett}{\end{quotesegment}\isabellestyle{it}\isastyle}
    1.43 -
    1.44 -% hack
    1.45 -\newcommand{\isasymSML}{SML}
    1.46 -
    1.47 -
    1.48 -%% contents
    1.49 -
    1.50  \title{\includegraphics[scale=0.5]{isabelle_isar}
    1.51    \\[4ex] Code generation from Isabelle/HOL theories}
    1.52  \author{\emph{Florian Haftmann}}
    1.53 @@ -75,7 +40,6 @@
    1.54  \input{Thy/document/ML.tex}
    1.55  
    1.56  \begingroup
    1.57 -%\tocentry{\bibname}
    1.58  \bibliographystyle{plain} \small\raggedright\frenchspacing
    1.59  \bibliography{../../manual}
    1.60  \endgroup
     2.1 --- a/doc-src/IsarAdvanced/Codegen/style.sty	Mon Dec 08 10:14:50 2008 +0100
     2.2 +++ b/doc-src/IsarAdvanced/Codegen/style.sty	Mon Dec 08 10:27:40 2008 +0100
     2.3 @@ -1,5 +1,3 @@
     2.4 -
     2.5 -%% $Id$
     2.6  
     2.7  %% toc
     2.8  \newcommand{\tocentry}[1]{\cleardoublepage\phantomsection\addcontentsline{toc}{chapter}{#1}
     2.9 @@ -7,15 +5,6 @@
    2.10  
    2.11  %% references
    2.12  \newcommand{\secref}[1]{\S\ref{#1}}
    2.13 -\newcommand{\chref}[1]{chapter~\ref{#1}}
    2.14 -\newcommand{\figref}[1]{figure~\ref{#1}}
    2.15 -
    2.16 -%% glossary
    2.17 -\renewcommand{\glossary}[2]{\nomenclature{\bf #1}{#2}}
    2.18 -\newcommand{\seeglossary}[1]{\emph{#1}}
    2.19 -\newcommand{\glossaryname}{Glossary}
    2.20 -\renewcommand{\nomname}{\glossaryname}
    2.21 -\renewcommand{\pagedeclaration}[1]{\nobreak\quad\dotfill~page~\bold{#1}}
    2.22  
    2.23  %% index
    2.24  \newcommand{\indexml}[1]{\index{\emph{#1}|bold}}
    2.25 @@ -23,38 +12,49 @@
    2.26  \newcommand{\indexmlstructure}[1]{\index{\emph{#1} (structure)|bold}}
    2.27  \newcommand{\indexmlfunctor}[1]{\index{\emph{#1} (functor)|bold}}
    2.28  
    2.29 -%% math
    2.30 -\newcommand{\text}[1]{\mbox{#1}}
    2.31 -\newcommand{\isasymvartheta}{\isamath{\theta}}
    2.32 -\newcommand{\isactrlvec}[1]{\emph{$\overline{#1}$}}
    2.33 +%% logical markup
    2.34 +\newcommand{\strong}[1]{{\bfseries {#1}}}
    2.35 +\newcommand{\qn}[1]{\emph{#1}}
    2.36 +
    2.37 +%% typographic conventions
    2.38 +\newcommand{\qt}[1]{``{#1}''}
    2.39 +
    2.40 +%% verbatim text
    2.41 +\newcommand{\isatypewriter}{\fontsize{9pt}{0pt}\tt\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{9pt}}
    2.42  
    2.43 +%% quoted segments
    2.44 +\makeatletter
    2.45 +\isakeeptag{quote}
    2.46 +\newenvironment{quotesegment}{\begin{quote}\isa@parindent\parindent\parindent0pt\isa@parskip\parskip\parskip0pt}{\end{quote}}
    2.47 +\renewcommand{\isatagquote}{\begin{quotesegment}}
    2.48 +\renewcommand{\endisatagquote}{\end{quotesegment}}
    2.49 +\makeatother
    2.50 +
    2.51 +\isakeeptag{quotett}
    2.52 +\renewcommand{\isatagquotett}{\begin{quotesegment}\isabellestyle{tt}\isastyle}
    2.53 +\renewcommand{\endisatagquotett}{\end{quotesegment}\isabellestyle{it}\isastyle}
    2.54 +
    2.55 +%% a trick
    2.56 +\newcommand{\isasymSML}{SML}
    2.57 +
    2.58 +%% presentation
    2.59  \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
    2.60  
    2.61  \pagestyle{headings}
    2.62 -\sloppy
    2.63  \binperiod
    2.64  \underscoreon
    2.65  
    2.66  \renewcommand{\isadigit}[1]{\isamath{#1}}
    2.67  
    2.68 +%% ml reference
    2.69  \newenvironment{mldecls}{\par\noindent\begingroup\footnotesize\def\isanewline{\\}\begin{tabular}{l}}{\end{tabular}\smallskip\endgroup}
    2.70  
    2.71 -\isafoldtag{FIXME}
    2.72  \isakeeptag{mlref}
    2.73  \renewcommand{\isatagmlref}{\subsection*{\makebox[0pt][r]{\fbox{\ML}~~}Reference}\begingroup\def\isastyletext{\rm}\small}
    2.74  \renewcommand{\endisatagmlref}{\endgroup}
    2.75  
    2.76 -\newcommand{\isasymGUESS}{\isakeyword{guess}}
    2.77 -\newcommand{\isasymOBTAIN}{\isakeyword{obtain}}
    2.78 -\newcommand{\isasymTHEORY}{\isakeyword{theory}}
    2.79 -\newcommand{\isasymUSES}{\isakeyword{uses}}
    2.80 -\newcommand{\isasymEND}{\isakeyword{end}}
    2.81 -\newcommand{\isasymCONSTS}{\isakeyword{consts}}
    2.82 -\newcommand{\isasymDEFS}{\isakeyword{defs}}
    2.83 -\newcommand{\isasymTHEOREM}{\isakeyword{theorem}}
    2.84 -\newcommand{\isasymDEFINITION}{\isakeyword{definition}}
    2.85 +\isabellestyle{it}
    2.86  
    2.87 -\isabellestyle{it}
    2.88  
    2.89  %%% Local Variables: 
    2.90  %%% mode: latex