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"];