| changeset 42 | f809cb54de4e |
| parent 30 | f5db9e08effc |
| child 62 | d94209ad2880 |
| 41:dbbc7989e753 | 42:f809cb54de4e |
|---|---|
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 use_thy "ListP";; |
6 no_document use_thy "ListP"; |
7 no_document use_thys ["../Prefix_subtract", "../Myhill_1"]; |