Pearl-jv/ROOT.ML
changeset 1789 7a99da5975e6
parent 1785 95df71c3df2f
child 2033 74bd7bfb484b
equal deleted inserted replaced
1788:22e6571d0bb2 1789:7a99da5975e6
       
     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"];