equal
deleted
inserted
replaced
88 * Isabelle/Isar reference manual provides more formal references in |
88 * Isabelle/Isar reference manual provides more formal references in |
89 syntax diagrams. |
89 syntax diagrams. |
90 |
90 |
91 |
91 |
92 *** HOL *** |
92 *** HOL *** |
|
93 |
|
94 * Theory Library/Saturated provides type of numbers with saturated |
|
95 arithmetic. |
93 |
96 |
94 * Classes bot and top require underlying partial order rather than |
97 * Classes bot and top require underlying partial order rather than |
95 preorder: uniqueness of bot and top is guaranteed. INCOMPATIBILITY. |
98 preorder: uniqueness of bot and top is guaranteed. INCOMPATIBILITY. |
96 |
99 |
97 * Class complete_lattice: generalized a couple of lemmas from sets; |
100 * Class complete_lattice: generalized a couple of lemmas from sets; |