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