changeset 2247 | d388a38f7198 |
parent 2073 | fb0655539d05 |
child 3511 | da4dd8b7ced4 |
2246:fce7e34db8c8 | 2247:d388a38f7198 |
---|---|
22 use_thy "Modal0"; |
22 use_thy "Modal0"; |
23 use_thy"T"; |
23 use_thy"T"; |
24 use_thy"S4"; |
24 use_thy"S4"; |
25 use_thy"S43"; |
25 use_thy"S43"; |
26 |
26 |
27 use "../Pure/install_pp.ML"; |
27 init_pps (); |
28 print_depth 8; |
28 print_depth 8; |
29 |
29 |
30 val Sequents_build_completed = (); (*indicate successful build*) |
30 val Sequents_build_completed = (); (*indicate successful build*) |