--- 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 "";
--- 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}
--- 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;