equal
deleted
inserted
replaced
141 primrec specifications have authentic syntax. |
141 primrec specifications have authentic syntax. |
142 |
142 |
143 * Library/Multiset: {#a, b, c#} abbreviates {#a#} + {#b#} + {#c#}. |
143 * Library/Multiset: {#a, b, c#} abbreviates {#a#} + {#b#} + {#c#}. |
144 |
144 |
145 * Library/ListVector: new theory of arithmetic vector operations. |
145 * Library/ListVector: new theory of arithmetic vector operations. |
|
146 |
|
147 * Library/Order_Relation: new theory of various orderings as sets of pairs. |
|
148 Defines preorders, partial orders, linear orders and well-orders |
|
149 on sets and on types. |
146 |
150 |
147 * Constants "card", "internal_split", "option_map" now with authentic |
151 * Constants "card", "internal_split", "option_map" now with authentic |
148 syntax. INCOMPATIBILITY. |
152 syntax. INCOMPATIBILITY. |
149 |
153 |
150 * Definitions subset_def, psubset_def, set_diff_def, Compl_def, |
154 * Definitions subset_def, psubset_def, set_diff_def, Compl_def, |