| changeset 7548 | 9e29a3af64ab |
| parent 7370 | 6407a09ac58f |
| child 7703 | 6b3424e877bd |
| 7547:a72a551b6d79 | 7548:9e29a3af64ab |
|---|---|
54 use_thy "Numeral"; |
54 use_thy "Numeral"; |
55 cd "Integ"; |
55 cd "Integ"; |
56 use_thy "IntDef"; |
56 use_thy "IntDef"; |
57 use "simproc.ML"; |
57 use "simproc.ML"; |
58 use_thy "NatBin"; |
58 use_thy "NatBin"; |
59 use "bin_simprocs.ML"; |
|
60 cd ".."; |
59 cd ".."; |
61 |
60 |
62 (*the all-in-one theory*) |
61 (*the all-in-one theory*) |
63 use_thy "Main"; |
62 use_thy "Main"; |
64 |
63 |