Pearl-jv/ROOT.ML
changeset 2742 f1192e3474e0
parent 2736 61d30863e5d1
child 2747 a5da7b6aff8f
equal deleted inserted replaced
2741:651355113eee 2742:f1192e3474e0
     1 no_document use_thys ["../Nominal/Nominal2_Base", 
       
     2                       "../Nominal/Atoms",
       
     3                       "../Nominal/Nominal2_Abs", 
       
     4                       "LaTeXsugar"];
       
     5 
     1 
     6 use_thys ["Paper"];
     2 use_thys ["../Nominal/Nominal2_Base", 
       
     3           "../Nominal/Atoms", 
       
     4           "../Nominal/Nominal2_Abs",
       
     5           "LaTeXsugar"];