src/HOL/Real/ROOT.ML

--- a/src/HOL/Real/ROOT.ML	Thu Nov 20 10:42:00 2003 +0100
+++ b/src/HOL/Real/ROOT.ML	Fri Nov 21 11:15:40 2003 +0100
@@ -7,5 +7,4 @@
 by Jacques Fleuriot
 *)
 
-no_document time_use_thy "Ring_and_Field";
 time_use_thy "Real";