--- a/src/HOL/Real/Hyperreal/ROOT.ML Fri Feb 05 21:06:24 1999 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,14 +0,0 @@
-(* Title: HOL/Hyperreal/ROOT
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1998 University of Cambridge
-
-Construction of the Hyperreals using ultrafilters, by Jacques Fleuriot
-*)
-
-HOL_build_completed; (*Make examples fail if HOL did*)
-
-writeln"Root file for HOL/Hyperreal";
-
-set proof_timing;
-time_use_thy "Filter";