Paper/ROOT.ML
changeset 754 b85875d65b10
child 1484 dc7b049d9072
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/ROOT.ML	Wed Dec 16 14:08:42 2009 +0100
@@ -0,0 +1,3 @@
+no_document use_thys ["../Quot/QuotMain"];
+
+use_thys ["Paper"];
\ No newline at end of file