tphols-2011/ROOT.ML
author urbanc
Tue, 08 Feb 2011 09:51:49 +0000
changeset 77 63bc9f9d96ba
parent 42 f809cb54de4e
permissions -rw-r--r--
small additions
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
(*
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
*)
42
f809cb54de4e Trying to solve the confict
zhang
parents: 39
diff changeset
     5
  use_thys ["../Myhill"];