equal
deleted
inserted
replaced
6 header {* Syntactic and abstract orders *} |
6 header {* Syntactic and abstract orders *} |
7 |
7 |
8 theory Orderings |
8 theory Orderings |
9 imports HOL |
9 imports HOL |
10 begin |
10 begin |
11 |
|
12 section {* Abstract orders *} |
|
13 |
11 |
14 subsection {* Order syntax *} |
12 subsection {* Order syntax *} |
15 |
13 |
16 class ord = |
14 class ord = |
17 fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<sqsubseteq>" 50) |
15 fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<sqsubseteq>" 50) |