quick_and_dirty := true;+
−
no_document use_thys ["Quotient", +
−
                      "~~/src/HOL/Library/LaTeXsugar",+
−
                      "~~/src/HOL/Quotient_Examples/FSet" ];+
−
use_thys ["Paper"];+
−