1
no_document use_thy "../Myhill";
2
no_document use_thy "~~/src/HOL/Library/LaTeXsugar";
3
4
use_thy "Paper"