src/HOLCF/IMP/document/root.tex
changeset 40774 0437dbc127b3
parent 40773 6c12f5e24e34
child 40775 ed7a4eadb2f6
     1.1 --- a/src/HOLCF/IMP/document/root.tex	Sat Nov 27 14:34:54 2010 -0800
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,36 +0,0 @@
     1.4 -
     1.5 -\documentclass[11pt,a4paper]{article}
     1.6 -\usepackage[latin1]{inputenc}
     1.7 -\usepackage{isabelle,isabellesym}
     1.8 -\usepackage{pdfsetup}
     1.9 -
    1.10 -\urlstyle{rm}
    1.11 -
    1.12 -% pretty printing for the Com language
    1.13 -%\newcommand{\CMD}[1]{\isatext{\bf\sffamily#1}}
    1.14 -\newcommand{\CMD}[1]{\isatext{\rm\sffamily#1}}
    1.15 -\newcommand{\isasymSKIP}{\CMD{skip}}
    1.16 -\newcommand{\isasymIF}{\CMD{if}}
    1.17 -\newcommand{\isasymTHEN}{\CMD{then}}
    1.18 -\newcommand{\isasymELSE}{\CMD{else}}
    1.19 -\newcommand{\isasymWHILE}{\CMD{while}}
    1.20 -\newcommand{\isasymDO}{\CMD{do}}
    1.21 -
    1.22 -\addtolength{\hoffset}{-1cm}
    1.23 -\addtolength{\textwidth}{2cm}
    1.24 -
    1.25 -\begin{document}
    1.26 -
    1.27 -\title{IMP in HOLCF}
    1.28 -\author{Tobias Nipkow and Robert Sandner}
    1.29 -\maketitle
    1.30 -
    1.31 -\tableofcontents
    1.32 -
    1.33 -\parindent 0pt\parskip 0.5ex
    1.34 -\input{session}
    1.35 -
    1.36 -\bibliographystyle{abbrv}
    1.37 -\bibliography{root}
    1.38 -
    1.39 -\end{document}