changeset 2237 | f01ac387e82b |
parent 1459 | d12da312eff4 |
child 3511 | da4dd8b7ced4 |
2236:c7869a443b14 | 2237:f01ac387e82b |
---|---|
18 use "../Provers/typedsimp.ML"; |
18 use "../Provers/typedsimp.ML"; |
19 use "rew.ML"; |
19 use "rew.ML"; |
20 use_thy "Arith"; |
20 use_thy "Arith"; |
21 use_thy "Bool"; |
21 use_thy "Bool"; |
22 |
22 |
23 use "../Pure/install_pp.ML"; |
23 init_pps (); |
24 print_depth 8; |
24 print_depth 8; |
25 |
25 |
26 val CTT_build_completed = (); (*indicate successful build*) |
26 val CTT_build_completed = (); (*indicate successful build*) |