equal
deleted
inserted
replaced
1 theory Matcher |
1 theory Matcher |
2 imports "Main" |
2 imports "Main" |
3 begin |
3 begin |
4 |
|
5 term "TYPE (nat * int)" |
|
6 term "TYPE ('a)" |
|
7 |
|
8 definition |
|
9 P:: "'a itself \<Rightarrow> bool" |
|
10 where |
|
11 "P (TYPE ('a)) \<equiv> ((\<lambda>x. (x::'a)) = (\<lambda>x. x))" |
|
12 |
|
13 |
4 |
14 section {* Sequential Composition of Sets *} |
5 section {* Sequential Composition of Sets *} |
15 |
6 |
16 definition |
7 definition |
17 Seq :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ;; _" [100,100] 100) |
8 Seq :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ;; _" [100,100] 100) |