diff -r 6ceb8d38bc9e -r 35fcab3da1b7 src/HOL/Extraction/document/root.tex
--- a/src/HOL/Extraction/document/root.tex	Tue Sep 07 11:51:53 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,27 +0,0 @@
-\documentclass[11pt,a4paper]{article}
-\usepackage{isabelle,isabellesym}
-\usepackage{pdfsetup}
-
-\urlstyle{rm}
-\isabellestyle{it}
-
-\begin{document}
-
-\title{Examples for program extraction in Higher-Order Logic}
-\author{Stefan Berghofer}
-\maketitle
-
-\nocite{Berger-JAR-2001,Coquand93}
-
-\tableofcontents
-\newcommand{\isasymbind}{\isamath{\mathbin{>\!\!\!>\mkern-6.7mu=}}}
-\newcommand{\isasymthen}{\isamath{\mathbin{>\!\!\!>}}}
-
-\parindent 0pt\parskip 0.5ex
-
-\input{session}
-
-\bibliographystyle{abbrv}
-\bibliography{root}
-
-\end{document}