changeset 62 | d94209ad2880 |
parent 42 | f809cb54de4e |
61:070f543e2560 | 62:d94209ad2880 |
---|---|
1 (* |
1 (* |
2 no_document use_thys ["This_Theory1", "This_Theory2"]; |
2 no_document use_thys ["This_Theory1", "This_Theory2"]; |
3 use_thys ["That_Theory1", "That_Theory2", "That_Theory3"]; |
3 use_thys ["That_Theory1", "That_Theory2", "That_Theory3"]; |
4 *) |
4 *) |
5 |
5 |
6 no_document use_thy "ListP"; |
6 use_thy "ListP"; |
7 no_document use_thys ["../Prefix_subtract", "../Myhill_1"]; |
7 use_thys ["../Prefix_subtract", "../Myhill_1", "../Myhill_2"]; |