equal
deleted
inserted
replaced
30 |
30 |
31 text {* |
31 text {* |
32 Sequential composition of two languages @{text "L1"} and @{text "L2"} |
32 Sequential composition of two languages @{text "L1"} and @{text "L2"} |
33 *} |
33 *} |
34 |
34 |
35 definition Seq :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ;; _" [100,100] 100) |
35 definition Seq :: "lang \<Rightarrow> lang \<Rightarrow> lang" ("_ ;; _" [100,100] 100) |
36 where |
36 where |
37 "L1 ;; L2 = {s1 @ s2 | s1 s2. s1 \<in> L1 \<and> s2 \<in> L2}" |
37 "L1 ;; L2 = {s1 @ s2 | s1 s2. s1 \<in> L1 \<and> s2 \<in> L2}" |
38 |
38 |
39 text {* Transitive closure of language @{text "L"}. *} |
39 text {* Transitive closure of language @{text "L"}. *} |
40 inductive_set |
40 inductive_set |