src/HOL/HOLCF/IMP/document/root.tex
author huffman
Sat, 27 Nov 2010 16:08:10 -0800
changeset 40774 0437dbc127b3
parent 12600 src/HOLCF/IMP/document/root.tex@30ec65eaaf5f
child 40945 b8703f63bfb2
permissions -rw-r--r--
moved directory src/HOLCF to src/HOL/HOLCF; added HOLCF theories to src/HOL/IsaMakefile;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
12430
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
     1
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
     2
\documentclass[11pt,a4paper]{article}
12600
wenzelm
parents: 12546
diff changeset
     3
\usepackage[latin1]{inputenc}
12430
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
     4
\usepackage{isabelle,isabellesym}
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
     5
\usepackage{pdfsetup}
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
     6
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
     7
\urlstyle{rm}
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
     8
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
     9
% pretty printing for the Com language
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    10
%\newcommand{\CMD}[1]{\isatext{\bf\sffamily#1}}
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    11
\newcommand{\CMD}[1]{\isatext{\rm\sffamily#1}}
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    12
\newcommand{\isasymSKIP}{\CMD{skip}}
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    13
\newcommand{\isasymIF}{\CMD{if}}
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    14
\newcommand{\isasymTHEN}{\CMD{then}}
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    15
\newcommand{\isasymELSE}{\CMD{else}}
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    16
\newcommand{\isasymWHILE}{\CMD{while}}
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    17
\newcommand{\isasymDO}{\CMD{do}}
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    18
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    19
\addtolength{\hoffset}{-1cm}
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    20
\addtolength{\textwidth}{2cm}
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    21
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    22
\begin{document}
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    23
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    24
\title{IMP in HOLCF}
12546
wenzelm
parents: 12430
diff changeset
    25
\author{Tobias Nipkow and Robert Sandner}
12430
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    26
\maketitle
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    27
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    28
\tableofcontents
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    29
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    30
\parindent 0pt\parskip 0.5ex
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    31
\input{session}
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    32
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    33
\bibliographystyle{abbrv}
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    34
\bibliography{root}
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    35
bfbd4d8faad7 latex output setup
kleing
parents:
diff changeset
    36
\end{document}