Quotient-Paper/ROOT.ML
changeset 2303 c785fff02a8f
parent 2186 762a739c9eb4
child 2368 d7dfe272b4f8
equal deleted inserted replaced
2302:c6db12ddb60c 2303:c785fff02a8f
     1 no_document use_thys ["Quotient", 
     1 no_document use_thys ["Quotient", 
     2                       "LaTeXsugar"];
     2                       "LaTeXsugar",
       
     3                       "../Nominal/FSet" ];
     3 
     4 
     4 use_thys ["Paper"];
     5 use_thys ["Paper"];