diff -r 660a4f5adee8 -r a6b0220fb8ae Quotient-Paper-jv/ROOT.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Quotient-Paper-jv/ROOT.ML	Tue Dec 20 17:54:53 2011 +0900
@@ -0,0 +1,5 @@
+quick_and_dirty := true;
+no_document use_thys ["Quotient", 
+                      "~~/src/HOL/Library/LaTeXsugar",
+                      "~~/src/HOL/Quotient_Examples/FSet" ];
+use_thys ["Paper"];