224 listsum_conv_fold, listsum_foldl, sort_foldl_insort, foldl_assoc, |
224 listsum_conv_fold, listsum_foldl, sort_foldl_insort, foldl_assoc, |
225 foldr_conv_foldl, start_le_sum, elem_le_sum, sum_eq_0_conv. |
225 foldr_conv_foldl, start_le_sum, elem_le_sum, sum_eq_0_conv. |
226 INCOMPATIBILITY. For the common phrases "%xs. List.foldr plus xs 0" |
226 INCOMPATIBILITY. For the common phrases "%xs. List.foldr plus xs 0" |
227 and "List.foldl plus 0", prefer "List.listsum". Otherwise it can |
227 and "List.foldl plus 0", prefer "List.listsum". Otherwise it can |
228 be useful to boil down "List.foldr" and "List.foldl" to "List.fold" |
228 be useful to boil down "List.foldr" and "List.foldl" to "List.fold" |
229 by unfolding "foldr_conv_fold" and "foldl_conv_fold". |
229 by unfolding "foldr_conv_fold" and "foldl_conv_fold". |
|
230 |
|
231 * Dropped lemmas minus_set_foldr, union_set_foldr, union_coset_foldr, |
|
232 inter_coset_foldr, Inf_fin_set_foldr, Sup_fin_set_foldr, |
|
233 Min_fin_set_foldr, Max_fin_set_foldr, Inf_set_foldr, Sup_set_foldr, |
|
234 INF_set_foldr, SUP_set_foldr. INCOMPATIBILITY. Prefer corresponding |
|
235 lemmas over fold rather than foldr, or make use of lemmas |
|
236 fold_conv_foldr and fold_rev. |
230 |
237 |
231 * Congruence rules Option.map_cong and Option.bind_cong for recursion |
238 * Congruence rules Option.map_cong and Option.bind_cong for recursion |
232 through option types. |
239 through option types. |
233 |
240 |
234 * Concrete syntax for case expressions includes constraints for source |
241 * Concrete syntax for case expressions includes constraints for source |