1 quick_and_dirty := true;

     2 no_document use_thys ["Quotient", 

     3                       "~~/src/HOL/Library/LaTeXsugar",

     4                       "~~/src/HOL/Quotient_Examples/FSet" ];

     5 use_thys ["Paper"];