src/Pure/Thy/ROOT.ML
author wenzelm
Tue, 02 Dec 1997 12:38:08 +0100
changeset 4339 b75312b2676d
parent 4214 523f6bea9fd7
child 4944 a6e71e5a1004
permissions -rw-r--r--
added context.ML;
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
390
b074205ac50a *** empty log message ***
wenzelm
parents: 74
diff changeset
     4
This file builds the theory parser and autoloading system.
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
4115
9405ebe284bf added path.ML;
wenzelm
parents: 4055
diff changeset
     7
use "path.ML";
4214
523f6bea9fd7 added file.ML, use.ML;
wenzelm
parents: 4115
diff changeset
     8
use "file.ML";
523f6bea9fd7 added file.ML, use.ML;
wenzelm
parents: 4115
diff changeset
     9
use "use.ML";
4115
9405ebe284bf added path.ML;
wenzelm
parents: 4055
diff changeset
    10
390
b074205ac50a *** empty log message ***
wenzelm
parents: 74
diff changeset
    11
use "thy_scan.ML";
b074205ac50a *** empty log message ***
wenzelm
parents: 74
diff changeset
    12
use "thy_parse.ML";
413
2a1554524ad5 removed garbage;
wenzelm
parents: 390
diff changeset
    13
use "thy_syn.ML";
3619
0fc67ad6d62a eliminated ThySynData and ThySynFun;
wenzelm
parents: 3600
diff changeset
    14
4339
b75312b2676d added context.ML;
wenzelm
parents: 4214
diff changeset
    15
use "context.ML";
b75312b2676d added context.ML;
wenzelm
parents: 4214
diff changeset
    16
3600
5366dde08dba Added some additional "use" commands for new files
berghofe
parents: 3576
diff changeset
    17
use "thy_info.ML";
5366dde08dba Added some additional "use" commands for new files
berghofe
parents: 3576
diff changeset
    18
use "browser_info.ML";
1132
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents: 1078
diff changeset
    19
use "thm_database.ML";
413
2a1554524ad5 removed garbage;
wenzelm
parents: 390
diff changeset
    20
use "thy_read.ML";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
4214
523f6bea9fd7 added file.ML, use.ML;
wenzelm
parents: 4115
diff changeset
    22
open ThmDatabase ThyRead ThyInfo BrowserInfo;