no_document use_thys ["../Nominal/Nominal2_Base", +− "../Nominal/Atoms", +− "~~/src/HOL/Library/LaTeXsugar"];+− +− use_thys ["Paper"];+−