no_document use_thys [ "~~/src/HOL/Library/LaTeXsugar", "~~/src/HOL/Library/OptionalSugar" ]; use_thy "Sugar";