author | paulson |
Wed, 25 Nov 1998 15:54:41 +0100 | |
changeset 5971 | c5a7a7685826 |
parent 5013 | 5b0c97631aff |
child 6210 | 465cae203337 |
permissions | -rw-r--r-- |
390 | 1 |
(* Title: Pure/Thy/ROOT.ML |
0 | 2 |
ID: $Id$ |
3 |
||
390 | 4 |
This file builds the theory parser and autoloading system. |
0 | 5 |
*) |
6 |
||
4214 | 7 |
use "use.ML"; |
4115 | 8 |
|
390 | 9 |
use "thy_scan.ML"; |
10 |
use "thy_parse.ML"; |
|
413 | 11 |
use "thy_syn.ML"; |
3619 | 12 |
|
4339 | 13 |
use "context.ML"; |
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 | 18 |
use "thy_read.ML"; |
0 | 19 |
|
4214 | 20 |
open ThmDatabase ThyRead ThyInfo BrowserInfo; |