no_document use_thy "../Myhill"; no_document use_thy "~~/src/HOL/Library/LaTeXsugar"; no_document use_thy "../Derivs"; no_document use_thy "../Closure"; use_thy "Paper"