src/Tools/WWW_Find/ROOT.ML
changeset 43075 6fde0c323c15
parent 43073 a4c985fe015d
child 43948 8f5add916a99
equal deleted inserted replaced
43074:8b566f0d226c 43075:6fde0c323c15
     9   use "socket_util.ML";
     9   use "socket_util.ML";
    10   use "scgi_req.ML";
    10   use "scgi_req.ML";
    11   use "scgi_server.ML";
    11   use "scgi_server.ML";
    12   use "echo.ML";
    12   use "echo.ML";
    13   use "html_templates.ML";
    13   use "html_templates.ML";
    14   use "find_theorems.ML")
    14   use "find_theorems.ML";
       
    15   use "yxml_find_theorems.ML")
    15 else ()
    16 else ()