doc-src/LaTeXsugar/Sugar/ROOT.ML
changeset 15337 628d87767434
child 15494 b09b68746eb6
equal deleted inserted replaced
15336:cb35ae957c65 15337:628d87767434
       
     1 use_thy "Sugar";
       
     2