# HG changeset patch
# User wu
# Date 1296219181 0
# Node ID 28d70591042a7b03fbd367090400aedf173fed3c
# Parent  7aa6c20e6d311d94aa0757cb5dcf2e17845c1c39
test

diff -r 7aa6c20e6d31 -r 28d70591042a Myhill_1.thy
--- a/Myhill_1.thy	Fri Jan 28 11:52:11 2011 +0000
+++ b/Myhill_1.thy	Fri Jan 28 12:53:01 2011 +0000
@@ -32,7 +32,7 @@
   Sequential composition of two languages @{text "L1"} and @{text "L2"} 
 *}
 
-definition Seq :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ;; _" [100,100] 100)
+definition Seq :: "lang \<Rightarrow> lang \<Rightarrow> lang" ("_ ;; _" [100,100] 100)
 where 
   "L1 ;; L2 = {s1 @ s2 | s1 s2. s1 \<in> L1 \<and> s2 \<in> L2}"
 
diff -r 7aa6c20e6d31 -r 28d70591042a tphols-2011/myhill.pdf
Binary file tphols-2011/myhill.pdf has changed