--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/ROOT.ML	Fri Jan 18 11:40:01 2013 +0000
@@ -0,0 +1,6 @@
+no_document 
+use_thys ["../thys/turing_basic", 
+          "../thys/uncomputable"(*, 
+          "../thys/abacus"*)];
+
+use_thys ["Paper"]