1
quick_and_dirty := true;
2
no_document use_thys ["~~/src/HOL/Library/LaTeXsugar",
3
"../Nominal/Nominal2"];
4
use_thys ["Paper"];