diff -r c0eac04ae3b4 -r c34347ec7ab3 Nominal-General/ROOT.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal-General/ROOT.ML	Sun Apr 04 21:39:28 2010 +0200
@@ -0,0 +1,7 @@
+
+no_document use_thys
+   ["Nominal2_Base",
+    "Nominal2_Eqvt",
+    "Nominal2_Atoms",
+    "Nominal2_Supp",
+    "Atoms"];