# HG changeset patch
# User wenzelm
# Date 1119025983 -7200
# Node ID 9aa6d9cf2832da501c5bfa50bf0394ca25591a46
# Parent  650ef3c13c4ddf16acdfdee86c864ff1d3ca36fb
obsolete;

diff -r 650ef3c13c4d -r 9aa6d9cf2832 src/HOL/Real/ex/document/root.tex
--- a/src/HOL/Real/ex/document/root.tex	Fri Jun 17 18:33:03 2005 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,20 +0,0 @@
-
-\documentclass[11pt,a4paper]{article}
-\usepackage[latin1]{inputenc}
-\usepackage{isabelle,isabellesym}
-\usepackage{pdfsetup}
-
-\urlstyle{rm}
-\isabellestyle{it}
-
-\begin{document}
-
-\title{Miscellaneous HOL-Real Examples}
-\maketitle
-
-\tableofcontents
-
-\parindent 0pt\parskip 0.5ex
-\input{session}
-
-\end{document}