changeset 21396 | afd8ba74313c |
parent 20507 | bb68343f6f83 |
child 21475 | ec0d1cf0eb35 |
21395:f34ac19659ae | 21396:afd8ba74313c |
---|---|
14 |
14 |
15 (*fake hiding of private structures*) |
15 (*fake hiding of private structures*) |
16 structure Hidden = struct end; |
16 structure Hidden = struct end; |
17 |
17 |
18 (*basic tools*) |
18 (*basic tools*) |
19 use "General/basics.ML"; |
|
19 use "library.ML"; |
20 use "library.ML"; |
20 cd "General"; use "ROOT.ML"; cd ".."; |
21 cd "General"; use "ROOT.ML"; cd ".."; |
21 |
22 |
22 (*fundamental structures*) |
23 (*fundamental structures*) |
23 use "name.ML"; |
24 use "name.ML"; |