equal
deleted
inserted
replaced
123 listsum_conv_fold, listsum_foldl, sort_foldl_insort. INCOMPATIBILITY. |
123 listsum_conv_fold, listsum_foldl, sort_foldl_insort. INCOMPATIBILITY. |
124 Prefer "List.fold" with canonical argument order, or boil down |
124 Prefer "List.fold" with canonical argument order, or boil down |
125 "List.foldr" and "List.foldl" to "List.fold" by unfolding "foldr_def" |
125 "List.foldr" and "List.foldl" to "List.fold" by unfolding "foldr_def" |
126 and "foldl_def". For the common phrases "%xs. List.foldr plus xs 0" |
126 and "foldl_def". For the common phrases "%xs. List.foldr plus xs 0" |
127 and "List.foldl plus 0", prefer "List.listsum". |
127 and "List.foldl plus 0", prefer "List.listsum". |
|
128 |
|
129 * Congruence rules Option.map_cong and Option.bind_cong for recursion |
|
130 through option types. |
128 |
131 |
129 * Concrete syntax for case expressions includes constraints for source |
132 * Concrete syntax for case expressions includes constraints for source |
130 positions, and thus produces Prover IDE markup for its bindings. |
133 positions, and thus produces Prover IDE markup for its bindings. |
131 INCOMPATIBILITY for old-style syntax translations that augment the |
134 INCOMPATIBILITY for old-style syntax translations that augment the |
132 pattern notation; e.g. see src/HOL/HOLCF/One.thy for translations of |
135 pattern notation; e.g. see src/HOL/HOLCF/One.thy for translations of |