src/Pure/Thy/ROOT.ML
author wenzelm
Mon, 06 Sep 1999 12:49:39 +0200
changeset 7484 9deae880cf74
parent 6346 643a1bd31a91
child 7723 7f073ed51193
permissions -rw-r--r--
added README;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
390
b074205ac50a *** empty log message ***
wenzelm
parents: 74
diff changeset
     1
(*  Title:      Pure/Thy/ROOT.ML
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
6210
465cae203337 tidied;
wenzelm
parents: 5013
diff changeset
     4
Theory system operations.
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
6210
465cae203337 tidied;
wenzelm
parents: 5013
diff changeset
     7
(*theory auto loader database*)
465cae203337 tidied;
wenzelm
parents: 5013
diff changeset
     8
use "thy_load.ML";
465cae203337 tidied;
wenzelm
parents: 5013
diff changeset
     9
use "thy_info.ML";
4115
9405ebe284bf added path.ML;
wenzelm
parents: 4055
diff changeset
    10
6210
465cae203337 tidied;
wenzelm
parents: 5013
diff changeset
    11
(*theory presentation*)
6323
e5b3e46d5dbd added html.ML, browser_info.ML;
wenzelm
parents: 6276
diff changeset
    12
use "html.ML";
e5b3e46d5dbd added html.ML, browser_info.ML;
wenzelm
parents: 6276
diff changeset
    13
use "browser_info.ML";
6210
465cae203337 tidied;
wenzelm
parents: 5013
diff changeset
    14
use "present.ML";
465cae203337 tidied;
wenzelm
parents: 5013
diff changeset
    15
use "thm_database.ML";
465cae203337 tidied;
wenzelm
parents: 5013
diff changeset
    16
6276
wenzelm
parents: 6210
diff changeset
    17
(*theory syntax (old format)*)
390
b074205ac50a *** empty log message ***
wenzelm
parents: 74
diff changeset
    18
use "thy_scan.ML";
b074205ac50a *** empty log message ***
wenzelm
parents: 74
diff changeset
    19
use "thy_parse.ML";
413
2a1554524ad5 removed garbage;
wenzelm
parents: 390
diff changeset
    20
use "thy_syn.ML";