changeset 2019 | b45d9f2042e0 |
parent 1982 | 38aafcab6890 |
child 2115 | 9709f9188549 |
2018:bcd69cc47cf0 | 2019:b45d9f2042e0 |
---|---|
36 use_thy "Inductive"; |
36 use_thy "Inductive"; |
37 |
37 |
38 use_thy "RelPow"; |
38 use_thy "RelPow"; |
39 use_thy "Finite"; |
39 use_thy "Finite"; |
40 use_thy "Sexp"; |
40 use_thy "Sexp"; |
41 use_thy "Option"; |
|
41 use_thy "List"; |
42 use_thy "List"; |
42 |
43 |
43 init_pps (); |
44 init_pps (); |
44 print_depth 8; |
45 print_depth 8; |
45 |
46 |