quick_and_dirty := true;+
−
no_document use_thys ["~~/src/HOL/Library/LaTeXsugar", +
−
                      "../Nominal/Nominal2"];+
−
use_thys ["Appendix"];+
−