src/Pure/Thy/ROOT.ML
author wenzelm
Sun Jul 23 12:10:11 2000 +0200 (2000-07-23)
changeset 9416 9144976964e7
parent 7764 9be1caad9782
child 11893 6b9e8820d4de
permissions -rw-r--r--
removed all_sessions.graph;
improved graph 'directories';
tuned;
     1 (*  Title:      Pure/Thy/ROOT.ML
     2     ID:         $Id$
     3 
     4 Theory system operations.
     5 *)
     6 
     7 (*theory auto loader database*)
     8 use "thy_load.ML";
     9 use "thy_info.ML";
    10 
    11 (*theory syntax -- old format*)
    12 use "thy_scan.ML";
    13 use "thy_parse.ML";
    14 use "thy_syn.ML";
    15 
    16 (*theory syntax -- new format*)
    17 use "../Isar/outer_lex.ML";
    18 
    19 (*theory presentation*)
    20 use "html.ML";
    21 use "latex.ML";
    22 use "present.ML";
    23 use "thm_deps.ML";
    24 
    25 (*theorem database -- user-level interface*)
    26 use "thm_database.ML";