| changeset 31 | b6815473ee2e |
| parent 30 | f5db9e08effc |
| child 37 | e4d0e6cdc3d2 |
| 30:f5db9e08effc | 31:b6815473ee2e |
|---|---|
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 ["../Myhill"];; |
5 use_thys ["../Prefix_subtract", "../Myhill"]; |