src/Pure/Thy/ROOT.ML
author paulson
Wed, 25 Nov 1998 15:54:41 +0100
changeset 5971 c5a7a7685826
parent 5013 5b0c97631aff
child 6210 465cae203337
permissions -rw-r--r--
simplified ensures_UNIV
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
4214
523f6bea9fd7 added file.ML, use.ML;
wenzelm
parents: 4115
diff changeset
     7
use "use.ML";
4115
9405ebe284bf added path.ML;
wenzelm
parents: 4055
diff changeset
     8
390
b074205ac50a *** empty log message ***
wenzelm
parents: 74
diff changeset
     9
use "thy_scan.ML";
b074205ac50a *** empty log message ***
wenzelm
parents: 74
diff changeset
    10
use "thy_parse.ML";
413
2a1554524ad5 removed garbage;
wenzelm
parents: 390
diff changeset
    11
use "thy_syn.ML";
3619
0fc67ad6d62a eliminated ThySynData and ThySynFun;
wenzelm
parents: 3600
diff changeset
    12
4339
b75312b2676d added context.ML;
wenzelm
parents: 4214
diff changeset
    13
use "context.ML";
b75312b2676d added context.ML;
wenzelm
parents: 4214
diff changeset
    14
3600
5366dde08dba Added some additional "use" commands for new files
berghofe
parents: 3576
diff changeset
    15
use "thy_info.ML";
5366dde08dba Added some additional "use" commands for new files
berghofe
parents: 3576
diff changeset
    16
use "browser_info.ML";
1132
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents: 1078
diff changeset
    17
use "thm_database.ML";
413
2a1554524ad5 removed garbage;
wenzelm
parents: 390
diff changeset
    18
use "thy_read.ML";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
4214
523f6bea9fd7 added file.ML, use.ML;
wenzelm
parents: 4115
diff changeset
    20
open ThmDatabase ThyRead ThyInfo BrowserInfo;