Pearl-jv/ROOT.ML
changeset 1785 95df71c3df2f
child 2033 74bd7bfb484b
equal deleted inserted replaced
1780:b7e524e7ee83 1785:95df71c3df2f
       
     1 no_document use_thys ["../Nominal-General/Nominal2_Base", 
       
     2                       "../Nominal-General/Nominal2_Atoms", 
       
     3                       "../Nominal-General/Nominal2_Eqvt",
       
     4                       "../Nominal-General/Atoms", 
       
     5                       "LaTeXsugar"];
       
     6 
       
     7 use_thys ["Paper"];