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