1 no_document use_thys ["../Nominal/Nominal2_Base", 

     1 no_document use_thys ["../Nominal/Nominal2_Base", 

     3                       "../Nominal/Atoms", 

     2                       "../Nominal/Atoms", 

     4                       "LaTeXsugar"];

     3                       "LaTeXsugar"];

     5 

     4 

     6 use_thys ["Paper"];

     5 use_thys ["Paper"];