1 no_document use_thys ["Quotient", 

     2 no_document use_thys ["Quotient", 

     2                       "LaTeXsugar",

     3                       "LaTeXsugar",

     3                       "../Nominal/FSet" ];

     4                       "../Nominal/FSet" ];

     4 

     5 

     5 use_thys ["Paper"];

     6 use_thys ["Paper"];