src/HOL/Real/ex/ROOT.ML

--- a/src/HOL/Real/ex/ROOT.ML	Tue May 06 12:29:49 2003 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,7 +0,0 @@
-(*  Title:      HOL/Real/ex/ROOT.ML
-    ID:         $Id$
-
-Miscellaneous HOL-Real Examples.
-*)
-
-time_use_thy "BinEx";