# HG changeset patch
# User wenzelm
# Date 1159479782 -7200
# Node ID 5855d1bbf2103816f288cf11d916f75468af40c9
# Parent  4eb07237382a1a238463626f49a740e12f7bfc1a
obsolete;

diff -r 4eb07237382a -r 5855d1bbf210 src/HOL/Isar_examples/Cantor.ML
--- a/src/HOL/Isar_examples/Cantor.ML	Thu Sep 28 23:43:00 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,20 +0,0 @@
-
-(* tactic script -- single steps *)
-
-Goal "EX S. S ~: range (f :: 'a => 'a set)";
-  by (rtac exI 1);
-  by (rtac notI 1);
-  by (etac rangeE 1);
-  by (etac equalityCE 1);
-  by (dtac CollectD 1);
-  by (contr_tac 1);
-  by (swap_res_tac [CollectI] 1);
-  by (assume_tac 1);
-qed "";
-
-
-(* tactic script -- automatic *)
-
-Goal "EX S. S ~: range (f :: 'a => 'a set)";
-  by (Best_tac 1);
-qed "";
diff -r 4eb07237382a -r 5855d1bbf210 src/HOL/Real/document/root.tex
--- a/src/HOL/Real/document/root.tex	Thu Sep 28 23:43:00 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,22 +0,0 @@
-
-% $Id$
-
-\documentclass[11pt,a4paper]{article}
-\usepackage{graphicx,isabelle,isabellesym,latexsym}
-\usepackage[latin1]{inputenc}
-\usepackage{pdfsetup}
-
-\urlstyle{rm}
-\isabellestyle{it}
-
-\begin{document}
-
-\title{Isabelle/HOL-Real --- Higher-Order Logic with Real Numbers}
-\maketitle
-
-\tableofcontents
-
-\parindent 0pt\parskip 0.5ex
-\input{session}
-
-\end{document}
diff -r 4eb07237382a -r 5855d1bbf210 src/HOLCF/HOLCF.ML
--- a/src/HOLCF/HOLCF.ML	Thu Sep 28 23:43:00 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,8 +0,0 @@
-(*  Title:      HOLCF/HOLCF.ML
-    ID:         $Id$
-*)
-
-structure HOLCF =
-struct
-  val thy = the_context ();
-end;