doc-src/IsarAdvanced/Codegen/codegen.tex
author haftmann
Mon Nov 03 14:15:25 2008 +0100 (2008-11-03)
changeset 28714 1992553cccfe
parent 28635 cc53d2ab0170
child 28727 185110a4b97a
permissions -rw-r--r--
improved verbatim mechanism
haftmann@20948
     1
haftmann@20948
     2
%% $Id$
haftmann@20948
     3
haftmann@20948
     4
\documentclass[12pt,a4paper,fleqn]{report}
haftmann@20948
     5
\usepackage{latexsym,graphicx}
haftmann@20948
     6
\usepackage[refpage]{nomencl}
haftmann@20948
     7
\usepackage{../../iman,../../extra,../../isar,../../proof}
wenzelm@26911
     8
\usepackage{../../isabelle,../../isabellesym}
haftmann@20948
     9
\usepackage{style}
haftmann@28635
    10
\usepackage{pgf}
haftmann@28635
    11
\usepackage{pgflibraryshapes}
haftmann@28560
    12
\usepackage{tikz}
wenzelm@26911
    13
\usepackage{../../pdfsetup}
haftmann@20948
    14
haftmann@28564
    15
%% setup
haftmann@28419
    16
haftmann@28569
    17
% hyphenation
haftmann@20948
    18
\hyphenation{Isabelle}
haftmann@20948
    19
\hyphenation{Isar}
haftmann@20948
    20
haftmann@28564
    21
% logical markup
haftmann@28564
    22
\newcommand{\strong}[1]{{\bfseries {#1}}}
haftmann@28564
    23
\newcommand{\qn}[1]{\emph{#1}}
haftmann@28564
    24
haftmann@28564
    25
% typographic conventions
haftmann@28564
    26
\newcommand{\qt}[1]{``{#1}''}
haftmann@28564
    27
haftmann@28564
    28
% verbatim text
haftmann@28714
    29
\newcommand{\isaverbatim}{\fontsize{9pt}{0pt}\tt\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{9pt}}
haftmann@28564
    30
haftmann@28564
    31
% invisibility
haftmann@20948
    32
\isadroptag{theory}
haftmann@28564
    33
haftmann@28564
    34
% quoted segments
haftmann@28564
    35
\makeatletter
haftmann@28564
    36
\isakeeptag{quote}
haftmann@28564
    37
\newenvironment{quotesegment}{\begin{quote}\isa@parindent\parindent\parindent0pt\isa@parskip\parskip\parskip0pt}{\end{quote}}
haftmann@28564
    38
\renewcommand{\isatagquote}{\begin{quotesegment}}
haftmann@28564
    39
\renewcommand{\endisatagquote}{\end{quotesegment}}
haftmann@28564
    40
\makeatother
haftmann@28564
    41
haftmann@28564
    42
\isakeeptag{quotett}
haftmann@28564
    43
\renewcommand{\isatagquotett}{\begin{quotesegment}\isabellestyle{tt}\isastyle}
haftmann@28564
    44
\renewcommand{\endisatagquotett}{\end{quotesegment}\isabellestyle{it}\isastyle}
haftmann@28564
    45
haftmann@28601
    46
% hack
haftmann@28601
    47
\newcommand{\isasymSML}{SML}
haftmann@28601
    48
haftmann@28564
    49
haftmann@28564
    50
%% contents
haftmann@28564
    51
haftmann@20948
    52
\title{\includegraphics[scale=0.5]{isabelle_isar}
haftmann@21222
    53
  \\[4ex] Code generation from Isabelle/HOL theories}
haftmann@20948
    54
\author{\emph{Florian Haftmann}}
haftmann@20948
    55
haftmann@20948
    56
\begin{document}
haftmann@20948
    57
haftmann@20948
    58
\maketitle
haftmann@20948
    59
haftmann@20948
    60
\begin{abstract}
haftmann@28447
    61
  This tutorial gives an introduction to a generic code generator framework in Isabelle
haftmann@28213
    62
  for generating executable code in functional programming languages from logical
haftmann@28213
    63
  specifications in Isabelle/HOL.
haftmann@20948
    64
\end{abstract}
haftmann@20948
    65
haftmann@20948
    66
\thispagestyle{empty}\clearpage
haftmann@20948
    67
haftmann@20948
    68
\pagenumbering{roman}
haftmann@20948
    69
\clearfirst
haftmann@20948
    70
haftmann@28419
    71
\input{Thy/document/Introduction.tex}
haftmann@28419
    72
\input{Thy/document/Program.tex}
haftmann@28419
    73
\input{Thy/document/Adaption.tex}
haftmann@28419
    74
\input{Thy/document/Further.tex}
haftmann@28419
    75
\input{Thy/document/ML.tex}
haftmann@20948
    76
haftmann@20948
    77
\begingroup
haftmann@20948
    78
%\tocentry{\bibname}
haftmann@20948
    79
\bibliographystyle{plain} \small\raggedright\frenchspacing
haftmann@20948
    80
\bibliography{../../manual}
haftmann@20948
    81
\endgroup
haftmann@20948
    82
haftmann@20948
    83
\end{document}
haftmann@20948
    84
haftmann@20948
    85
haftmann@20948
    86
%%% Local Variables: 
haftmann@20948
    87
%%% mode: latex
haftmann@20948
    88
%%% TeX-master: t
haftmann@20948
    89
%%% End: