changeset 37 | e4d0e6cdc3d2 |
parent 31 | b6815473ee2e |
child 39 | a59473f0229d |
36:f5cc33a0ba99 | 37:e4d0e6cdc3d2 |
---|---|
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 use_thys ["../Prefix_subtract", "../Myhill"]; |
5 |
6 no_document use_thys ["../Prefix_subtract"]; |
|
7 |
|
8 use_thys ["../Myhill"]; |