changeset 13305 | f88d0c363582 |
parent 12582 | b85acd66f715 |
13304:43ef6c6dd906 | 13305:f88d0c363582 |
---|---|
1 use "../settings.ML"; |
1 use "../settings.ML"; |
2 use_thy "Tree"; |
2 use_thy "Tree"; |
3 use_thy "Tree2"; |
3 use_thy "Tree2"; |
4 use_thy "Plus"; |
|
4 use_thy "case_exprs"; |
5 use_thy "case_exprs"; |
5 use_thy "fakenat"; |
6 use_thy "fakenat"; |
6 use_thy "natsum"; |
7 use_thy "natsum"; |
7 use_thy "pairs"; |
8 use_thy "pairs"; |
8 use_thy "Option2"; |
9 use_thy "Option2"; |