equal
deleted
inserted
replaced
10 |
10 |
11 theory Semilat |
11 theory Semilat |
12 imports Main "~~/src/HOL/Library/While_Combinator" |
12 imports Main "~~/src/HOL/Library/While_Combinator" |
13 begin |
13 begin |
14 |
14 |
15 types |
15 type_synonym 'a ord = "'a \<Rightarrow> 'a \<Rightarrow> bool" |
16 'a ord = "'a \<Rightarrow> 'a \<Rightarrow> bool" |
16 type_synonym 'a binop = "'a \<Rightarrow> 'a \<Rightarrow> 'a" |
17 'a binop = "'a \<Rightarrow> 'a \<Rightarrow> 'a" |
17 type_synonym 'a sl = "'a set \<times> 'a ord \<times> 'a binop" |
18 'a sl = "'a set \<times> 'a ord \<times> 'a binop" |
|
19 |
18 |
20 consts |
19 consts |
21 "lesub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" |
20 "lesub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" |
22 "lesssub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" |
21 "lesssub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" |
23 "plussub" :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c" |
22 "plussub" :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c" |