diff -r 9df6144e281b -r 853abc14c5c6 Nominal/ROOT.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/ROOT.ML	Thu Feb 25 08:40:52 2010 +0100
@@ -0,0 +1,8 @@
+quick_and_dirty := true;
+
+no_document use_thys
+   ["Nominal2_Base",
+    "Nominal2_Eqvt",
+    "Nominal2_Atoms",
+    "Nominal2_Supp",
+    "Test"];