equal
deleted
inserted
replaced
23 cd "General"; use "ROOT.ML"; cd ".."; |
23 cd "General"; use "ROOT.ML"; cd ".."; |
24 |
24 |
25 (*concurrency within the ML runtime*) |
25 (*concurrency within the ML runtime*) |
26 use "Concurrent/mailbox.ML"; |
26 use "Concurrent/mailbox.ML"; |
27 use "Concurrent/schedule.ML"; |
27 use "Concurrent/schedule.ML"; |
|
28 use "Concurrent/future.ML"; |
28 |
29 |
29 (*fundamental structures*) |
30 (*fundamental structures*) |
30 use "name.ML"; |
31 use "name.ML"; |
31 use "term.ML"; |
32 use "term.ML"; |
32 use "term_subst.ML"; |
33 use "term_subst.ML"; |