| author | zhang |
| Tue, 25 Jan 2011 12:14:31 +0000 | |
| changeset 31 | b6815473ee2e |
| parent 30 | f5db9e08effc |
| child 37 | e4d0e6cdc3d2 |
| 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 |
*) |
|
31
b6815473ee2e
1. Myhill.thy is proved to correct some typos. 2. Some sections are added to the first direction. 3. The small theory of list difference is now separated into Prefix_subtract.thy and the ROOT.ML
zhang
parents:
30
diff
changeset
|
5 |
use_thys ["../Prefix_subtract", "../Myhill"]; |