src/Pure/Thy/ROOT.ML
changeset 4214 523f6bea9fd7
parent 4115 9405ebe284bf
child 4339 b75312b2676d
equal deleted inserted replaced
4213:cef5ef41e70d 4214:523f6bea9fd7
     5 
     5 
     6 This file builds the theory parser and autoloading system.
     6 This file builds the theory parser and autoloading system.
     7 *)
     7 *)
     8 
     8 
     9 use "path.ML";
     9 use "path.ML";
       
    10 use "file.ML";
       
    11 use "use.ML";
    10 
    12 
    11 use "thy_scan.ML";
    13 use "thy_scan.ML";
    12 use "thy_parse.ML";
    14 use "thy_parse.ML";
    13 use "thy_syn.ML";
    15 use "thy_syn.ML";
    14 
    16 
    15 use "thy_info.ML";
    17 use "thy_info.ML";
    16 use "browser_info.ML";
    18 use "browser_info.ML";
    17 use "thm_database.ML";
    19 use "thm_database.ML";
    18 
       
    19 use "symbol_input.ML";
       
    20 use "thy_read.ML";
    20 use "thy_read.ML";
    21 
    21 
    22 open ThmDatabase ThyRead ThyInfo BrowserInfo SymbolInput;
    22 open ThmDatabase ThyRead ThyInfo BrowserInfo;
    23 
    23 
    24 
    24 
    25 
    25 
    26 (* FIXME tmp, move *)
    26 (* FIXME tmp, move *)
    27 
    27