# HG changeset patch
# User wenzelm
# Date 860155060 -7200
# Node ID c0abd2fd9b7c5a66767d60000745069d7ac29b43
# Parent  d7bff1252d1ea45f4df96554653b651d424fcb5a
*** empty log message ***

diff -r d7bff1252d1e -r c0abd2fd9b7c src/HOL/Quot/ROOT.ML
--- a/src/HOL/Quot/ROOT.ML	Fri Apr 04 13:56:11 1997 +0200
+++ b/src/HOL/Quot/ROOT.ML	Fri Apr 04 13:57:40 1997 +0200
@@ -10,4 +10,5 @@
 
 writeln"Root file for HOL/Quot";
 
-use_thy "Quot";
+(*use_thy "Quot";*)
+