1 quick_and_dirty := true;

     2 no_document use_thys ["~~/src/HOL/Library/LaTeXsugar", 

     3                       "../Nominal/Nominal2"];

     4 use_thys ["Paper"];