--- 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}"
Binary file tphols-2011/myhill.pdf has changed