equal
deleted
inserted
replaced
57 * Isabelle/Isar reference manual provides more formal references in |
57 * Isabelle/Isar reference manual provides more formal references in |
58 syntax diagrams. |
58 syntax diagrams. |
59 |
59 |
60 |
60 |
61 *** HOL *** |
61 *** HOL *** |
|
62 |
|
63 * classes bot and top require underlying partial order rather than preorder: |
|
64 uniqueness of bot and top is guaranteed. INCOMPATIBILITY. |
62 |
65 |
63 * Archimedian_Field.thy: |
66 * Archimedian_Field.thy: |
64 floor now is defined as parameter of a separate type class floor_ceiling. |
67 floor now is defined as parameter of a separate type class floor_ceiling. |
65 |
68 |
66 * Finite_Set.thy: more coherent development of fold_set locales: |
69 * Finite_Set.thy: more coherent development of fold_set locales: |