test
authorwu
Fri, 28 Jan 2011 12:53:01 +0000
changeset 46 28d70591042a
parent 45 7aa6c20e6d31
child 47 bea2466a6084
test
Myhill_1.thy
tphols-2011/myhill.pdf
--- 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