src/HOL/IMP/document/root.tex
author krauss
Fri Nov 24 13:44:51 2006 +0100 (2006-11-24)
changeset 21512 3786eb1b69d6
parent 12546 0c90e581379f
child 43141 11fce8564415
permissions -rw-r--r--
Lemma "fundef_default_value" uses predicate instead of set.
     1 
     2 \documentclass[a4wide]{article}
     3 \usepackage{graphicx,isabelle,isabellesym}
     4 \usepackage{pdfsetup}
     5 
     6 \urlstyle{rm}
     7 \renewcommand{\isachardoublequote}{}
     8 
     9 % pretty printing for the Com language
    10 %\newcommand{\CMD}[1]{\isatext{\bf\sffamily#1}}
    11 \newcommand{\CMD}[1]{\isatext{\rm\sffamily#1}}
    12 \newcommand{\isasymSKIP}{\CMD{skip}}
    13 \newcommand{\isasymIF}{\CMD{if}}
    14 \newcommand{\isasymTHEN}{\CMD{then}}
    15 \newcommand{\isasymELSE}{\CMD{else}}
    16 \newcommand{\isasymWHILE}{\CMD{while}}
    17 \newcommand{\isasymDO}{\CMD{do}}
    18 
    19 \addtolength{\hoffset}{-1cm}
    20 \addtolength{\textwidth}{2cm}
    21 
    22 \begin{document}
    23 
    24 \title{IMP --- A {\tt WHILE}-language and its Semantics}
    25 \author{Gerwin Klein, Heiko Loetzbeyer, Tobias Nipkow, Robert Sandner}
    26 \maketitle
    27 
    28 \parindent 0pt\parskip 0.5ex
    29 
    30 \begin{abstract}\noindent
    31   The denotational, operational, and axiomatic semantics, a verification
    32   condition generator, and all the necessary soundness, completeness and
    33   equivalence proofs. Essentially a formalization of the first 100 pages of
    34   \cite{Winskel}.
    35   
    36   An eminently readable description of this theory is found in \cite{Nipkow}.
    37   See also HOLCF/IMP for a denotational semantics.
    38 \end{abstract}
    39 
    40 \tableofcontents
    41 
    42 \begin{center}
    43   \includegraphics[scale=0.7]{session_graph}
    44 \end{center}
    45 
    46 \parindent 0pt\parskip 0.5ex
    47 \input{session}
    48 
    49 \bibliographystyle{plain}
    50 \bibliography{root}
    51 
    52 \end{document}