--- a/Paper/ROOT.ML	Sat Jan 19 14:29:56 2013 +0000
+++ b/Paper/ROOT.ML	Sat Jan 19 14:44:07 2013 +0000
@@ -1,5 +1,6 @@
 no_document 
 use_thys ["../thys/turing_basic", 
+          "../thys/turing_hoare",
           "../thys/uncomputable"(*, 
           "../thys/abacus"*)];