src/HOL/Real/ex/ROOT.ML

--- a/src/HOL/Real/ex/ROOT.ML	Thu Sep 27 18:45:23 2001 +0200
+++ b/src/HOL/Real/ex/ROOT.ML	Thu Sep 27 18:45:40 2001 +0200
@@ -1,9 +1,9 @@
 (*  Title:      HOL/Real/ex/ROOT.ML
     ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1999  University of Cambridge
 
-HOL/Real examples.
+Miscellaneous HOL-Real Examples.
 *)
 
+no_document use_thy "Primes";
+time_use_thy "Sqrt_Irrational";
 time_use_thy "BinEx";