equal
deleted
inserted
replaced
3 imports "Main" |
3 imports "Main" |
4 begin |
4 begin |
5 |
5 |
6 |
6 |
7 section {* Sequential Composition of Sets *} |
7 section {* Sequential Composition of Sets *} |
8 m |
8 |
9 definition |
9 definition |
10 Sequ :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ;; _" [100,100] 100) |
10 Sequ :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ;; _" [100,100] 100) |
11 where |
11 where |
12 "A ;; B = {s1 @ s2 | s1 s2. s1 \<in> A \<and> s2 \<in> B}" |
12 "A ;; B = {s1 @ s2 | s1 s2. s1 \<in> A \<and> s2 \<in> B}" |
13 |
13 |