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