author | zhang |
Thu, 27 Jan 2011 12:35:06 +0000 | |
changeset 42 | f809cb54de4e |
parent 30 | f5db9e08effc |
child 62 | d94209ad2880 |
permissions | -rw-r--r-- |
30
f5db9e08effc
Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy].
zhang
parents:
diff
changeset
|
1 |
(* |
f5db9e08effc
Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy].
zhang
parents:
diff
changeset
|
2 |
no_document use_thys ["This_Theory1", "This_Theory2"]; |
f5db9e08effc
Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy].
zhang
parents:
diff
changeset
|
3 |
use_thys ["That_Theory1", "That_Theory2", "That_Theory3"]; |
f5db9e08effc
Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy].
zhang
parents:
diff
changeset
|
4 |
*) |
f5db9e08effc
Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy].
zhang
parents:
diff
changeset
|
5 |
|
42 | 6 |
no_document use_thy "ListP"; |
7 |
no_document use_thys ["../Prefix_subtract", "../Myhill_1"]; |