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