changeset 484 | 70b789956bd3 |
parent 435 | ca5356bd315a |
child 488 | 52f7447d4f1b |
483:4d1614d8f119 | 484:70b789956bd3 |
---|---|
26 |
26 |
27 fun DO_GOAL tfs = SELECT_GOAL (CHECK_SOLVED (EVERY1 tfs)); |
27 fun DO_GOAL tfs = SELECT_GOAL (CHECK_SOLVED (EVERY1 tfs)); |
28 |
28 |
29 print_depth 1; |
29 print_depth 1; |
30 |
30 |
31 use_thy "CardinalArith"; |
31 use_thy "Cardinal_AC"; |
32 use_thy "Fin"; |
|
33 use_thy "ListFn"; |
32 use_thy "ListFn"; |
34 |
33 |
35 (*printing functions are inherited from FOL*) |
34 (*printing functions are inherited from FOL*) |
36 print_depth 8; |
35 print_depth 8; |
37 |
36 |