equal
deleted
inserted
replaced
5 Most congruence rules by Stephan Hohe. |
5 Most congruence rules by Stephan Hohe. |
6 With additional contributions from Alasdair Armstrong and Simon Foster. |
6 With additional contributions from Alasdair Armstrong and Simon Foster. |
7 *) |
7 *) |
8 |
8 |
9 theory Order |
9 theory Order |
10 imports |
10 imports |
11 "HOL-Library.FuncSet" |
11 Congruence |
12 Congruence |
|
13 begin |
12 begin |
14 |
13 |
15 section \<open>Orders\<close> |
14 section \<open>Orders\<close> |
16 |
15 |
17 subsection \<open>Partial Orders\<close> |
16 subsection \<open>Partial Orders\<close> |