# HG changeset patch # User wu # Date 1296082704 0 # Node ID e4d0e6cdc3d28051783b838eecfc9a2ef06271b0 # Parent f5cc33a0ba9968fe8ff0eebc12726ae789d02a40 ITP-Paper loads Myhill.thy diff -r f5cc33a0ba99 -r e4d0e6cdc3d2 Paper/Paper.thy --- a/Paper/Paper.thy Wed Jan 26 22:51:51 2011 +0000 +++ b/Paper/Paper.thy Wed Jan 26 22:58:24 2011 +0000 @@ -1,6 +1,6 @@ (*<*) theory Paper -imports Main +imports "../Myhill" begin (*>*) diff -r f5cc33a0ba99 -r e4d0e6cdc3d2 Paper/ROOT.ML --- a/Paper/ROOT.ML Wed Jan 26 22:51:51 2011 +0000 +++ b/Paper/ROOT.ML Wed Jan 26 22:58:24 2011 +0000 @@ -1,2 +1,4 @@ +no_document use_thy "../Myhill"; no_document use_thy "LaTeXsugar"; + use_thy "Paper" \ No newline at end of file diff -r f5cc33a0ba99 -r e4d0e6cdc3d2 tphols-2011/ROOT.ML --- a/tphols-2011/ROOT.ML Wed Jan 26 22:51:51 2011 +0000 +++ b/tphols-2011/ROOT.ML Wed Jan 26 22:58:24 2011 +0000 @@ -2,4 +2,7 @@ no_document use_thys ["This_Theory1", "This_Theory2"]; use_thys ["That_Theory1", "That_Theory2", "That_Theory3"]; *) - use_thys ["../Prefix_subtract", "../Myhill"]; + +no_document use_thys ["../Prefix_subtract"]; + +use_thys ["../Myhill"]; diff -r f5cc33a0ba99 -r e4d0e6cdc3d2 tphols-2011/myhill.pdf Binary file tphols-2011/myhill.pdf has changed