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