ROOT2.ML
changeset 2 301f567e2a8e
equal deleted inserted replaced
1:dcde836219bc 2:301f567e2a8e
       
     1 
       
     2 no_document use_thy "~~/src/HOL/Library/LaTeXsugar";
       
     3 
       
     4 use_thy "Paper";