changeset 393 | 02b27671b899 |
parent 121 | d392174734e9 |
child 1294 | 1358dc040edb |
392:674d878719bd | 393:02b27671b899 |
---|---|
10 val banner = "Constructive Type Theory"; |
10 val banner = "Constructive Type Theory"; |
11 writeln banner; |
11 writeln banner; |
12 |
12 |
13 print_depth 1; |
13 print_depth 1; |
14 |
14 |
15 structure Readthy = ReadthyFUN (structure ThySyn = ThySyn); |
15 init_thy_reader(); |
16 open Readthy; |
|
17 |
16 |
18 use_thy "CTT"; |
17 use_thy "CTT"; |
19 use "../Provers/typedsimp.ML"; |
18 use "../Provers/typedsimp.ML"; |
20 use "rew.ML"; |
19 use "rew.ML"; |
21 use_thy "Arith"; |
20 use_thy "Arith"; |