author | nipkow |
Thu, 29 Apr 1999 18:33:31 +0200 | |
changeset 6539 | 2e7d2fba9f6c |
parent 6346 | 643a1bd31a91 |
child 7723 | 7f073ed51193 |
permissions | -rw-r--r-- |
390 | 1 |
(* Title: Pure/Thy/ROOT.ML |
0 | 2 |
ID: $Id$ |
3 |
||
6210 | 4 |
Theory system operations. |
0 | 5 |
*) |
6 |
||
6210 | 7 |
(*theory auto loader database*) |
8 |
use "thy_load.ML"; |
|
9 |
use "thy_info.ML"; |
|
4115 | 10 |
|
6210 | 11 |
(*theory presentation*) |
6323 | 12 |
use "html.ML"; |
13 |
use "browser_info.ML"; |
|
6210 | 14 |
use "present.ML"; |
15 |
use "thm_database.ML"; |
|
16 |
||
6276 | 17 |
(*theory syntax (old format)*) |
390 | 18 |
use "thy_scan.ML"; |
19 |
use "thy_parse.ML"; |
|
413 | 20 |
use "thy_syn.ML"; |