no_document use_thy "../Myhill";+− no_document use_thy "~~/src/HOL/Library/LaTeXsugar";+− +− use_thy "Paper"+−