| changeset 48536 | 4e2ee88276d2 |
| parent 48535 | 619531d87ce4 |
| parent 48528 | 784c6f63d79c |
| child 48537 | ba0dd46b9214 |
| 48535:619531d87ce4 | 48536:4e2ee88276d2 |
|---|---|
1 use "../settings.ML"; |
|
2 use_thy "Tree"; |
|
3 use_thy "Tree2"; |
|
4 use_thy "Plus"; |
|
5 use_thy "case_exprs"; |
|
6 use_thy "fakenat"; |
|
7 use_thy "natsum"; |
|
8 use_thy "pairs"; |
|
9 use_thy "Option2"; |
|
10 use_thy "types"; |
|
11 use_thy "prime_def"; |
|
12 use_thy "simp"; |
|
13 use_thy "Itrev"; |
|
14 use_thy "AdvancedInd"; |
|
15 use_thy "appendix"; |