Paper/ROOT.ML
changeset 754 b85875d65b10
child 1484 dc7b049d9072
equal deleted inserted replaced
751:670131bcba4a 754:b85875d65b10
       
     1 no_document use_thys ["../Quot/QuotMain"];
       
     2 
       
     3 use_thys ["Paper"];