changeset 39 | a59473f0229d |
parent 37 | e4d0e6cdc3d2 |
child 42 | f809cb54de4e |
38:a1268fb0deea | 39:a59473f0229d |
---|---|
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_thys ["../Prefix_subtract"]; |
6 no_document use_thys ["../Prefix_subtract", "../Prelude"]; |
7 |
7 |
8 use_thys ["../Myhill"]; |
8 use_thys ["../Myhill"]; |