src/HOL/Imperative_HOL/ROOT.ML
changeset 41413 64cd30d6b0b8
parent 39307 8d42d668b5b0
--- a/src/HOL/Imperative_HOL/ROOT.ML	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Imperative_HOL/ROOT.ML	Wed Dec 29 17:34:41 2010 +0100
@@ -1,4 +1,7 @@
-
-no_document use_thys ["Countable", "Monad_Syntax", "Code_Natural", "LaTeXsugar"];
+no_document use_thys [
+  "~~/src/HOL/Library/Countable",
+  "~~/src/HOL/Library/Monad_Syntax",
+  "~~/src/HOL/Library/Code_Natural",
+  "~~/src/HOL/Library/LaTeXsugar"];
 
 use_thys ["Imperative_HOL_ex"];