# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1267616755 -3600
# Node ID 531dcebbf48364544f1fa9f5e8abb88631f3630d
# Parent  670701b19e8e28f2dd91df8381f26f3936d6efce
start of paper - does not compile yet

diff -r 670701b19e8e -r 531dcebbf483 Paper/document/root.tex
--- a/Paper/document/root.tex	Wed Mar 03 11:50:25 2010 +0100
+++ b/Paper/document/root.tex	Wed Mar 03 12:45:55 2010 +0100
@@ -1,4 +1,4 @@
-\documentclass[11pt,a4paper]{article}
+\documentstyle[epsf]{acmconf}
 \usepackage{isabelle,isabellesym}
 
 % further packages required for unusual symbols (see also
@@ -36,19 +36,30 @@
 % for uniform font size
 %\renewcommand{\isastyle}{\isastyleminor}
 
+%----------------- theorem definitions ----------
+\newtheorem{Theorem}{Theorem}[section]
+\newtheorem{Definition}[Theorem]{Definition}
+\newtheorem{Example}{\it Example}[section]
+
+%-------------------- environment definitions -----------------
+\newenvironment{example}[0]{\begin{Example} \it}{\end{Example}}
+\newenvironment{proof-of}[1]{{\em Proof of #1:}}{}
 
 \begin{document}
 
-\title{Paper}
-\author{By Kaliszyk and Urban}
+\title{\LARGE\bf General Binding Structures in Nominal Isabelle, or How to
+  Formalise Core-Haskell}
 \maketitle
 
-% sane default for proof documents
-\parindent 0pt\parskip 0.5ex
+\maketitle
+\begin{abstract} 
+TODO
+\end{abstract}
 
 % generated text of all theories
 \input{session}
 
+%\bibliographystyle{plain}
 % optional bibliography
 %\bibliographystyle{abbrv}
 %\bibliography{root}