equal
deleted
inserted
replaced
9 imports HOL |
9 imports HOL |
10 begin |
10 begin |
11 |
11 |
12 subsection {* Order syntax *} |
12 subsection {* Order syntax *} |
13 |
13 |
14 class ord = |
14 class ord = type + |
15 fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<sqsubseteq>" 50) |
15 fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<sqsubseteq>" 50) |
16 and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<sqsubset>" 50) |
16 and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<sqsubset>" 50) |
17 begin |
17 begin |
18 |
18 |
19 notation |
19 notation |