pres/ListP.thy
author urbanc
Thu, 11 Aug 2011 23:11:39 +0000
changeset 193 2a5ac68db24b
parent 30 f5db9e08effc
permissions -rw-r--r--
finished section about derivatives and closure properties
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
theory ListP
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
imports Main List_Prefix
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
begin
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
end