changeset 4024 | 3c056eab237c |
parent 3941 | ea440c63d206 |
child 4905 | be73ddff6c5a |
4023:a9dc0484c903 | 4024:3c056eab237c |
---|---|
9 *) |
9 *) |
10 |
10 |
11 val banner = "Logic for Computable Functions (in FOL)"; |
11 val banner = "Logic for Computable Functions (in FOL)"; |
12 writeln banner; |
12 writeln banner; |
13 |
13 |
14 reset global_names; |
|
15 |
|
16 print_depth 1; |
14 print_depth 1; |
17 use_thy "LCF"; |
15 use_thy "LCF"; |
18 use"simpdata.ML"; |
16 use"simpdata.ML"; |
19 use"pair.ML"; |
17 use"pair.ML"; |
20 use"fix.ML"; |
18 use"fix.ML"; |