equal
deleted
inserted
replaced
228 val gen_merge_lists: ('a * 'a -> bool) -> 'a list -> 'a list -> 'a list |
228 val gen_merge_lists: ('a * 'a -> bool) -> 'a list -> 'a list -> 'a list |
229 val gen_merge_lists': ('a * 'a -> bool) -> 'a list -> 'a list -> 'a list |
229 val gen_merge_lists': ('a * 'a -> bool) -> 'a list -> 'a list -> 'a list |
230 val merge_lists: ''a list -> ''a list -> ''a list |
230 val merge_lists: ''a list -> ''a list -> ''a list |
231 val merge_lists': ''a list -> ''a list -> ''a list |
231 val merge_lists': ''a list -> ''a list -> ''a list |
232 val merge_alists: (''a * 'b) list -> (''a * 'b) list -> (''a * 'b) list |
232 val merge_alists: (''a * 'b) list -> (''a * 'b) list -> (''a * 'b) list |
|
233 val merge_alists': (''a * 'b) list -> (''a * 'b) list -> (''a * 'b) list |
233 |
234 |
234 (*balanced trees*) |
235 (*balanced trees*) |
235 exception Balance |
236 exception Balance |
236 val fold_bal: ('a * 'a -> 'a) -> 'a list -> 'a |
237 val fold_bal: ('a * 'a -> 'a) -> 'a list -> 'a |
237 val access_bal: ('a -> 'a) * ('a -> 'a) * 'a -> int -> int -> 'a |
238 val access_bal: ('a -> 'a) * ('a -> 'a) * 'a -> int -> int -> 'a |
1070 | gen_merge_lists' eq xs ys = gen_rems eq (ys, xs) @ xs; |
1071 | gen_merge_lists' eq xs ys = gen_rems eq (ys, xs) @ xs; |
1071 |
1072 |
1072 fun merge_lists xs ys = gen_merge_lists (op =) xs ys; |
1073 fun merge_lists xs ys = gen_merge_lists (op =) xs ys; |
1073 fun merge_lists' xs ys = gen_merge_lists' (op =) xs ys; |
1074 fun merge_lists' xs ys = gen_merge_lists' (op =) xs ys; |
1074 fun merge_alists al = gen_merge_lists eq_fst al; |
1075 fun merge_alists al = gen_merge_lists eq_fst al; |
|
1076 fun merge_alists' al = gen_merge_lists' eq_fst al; |
1075 |
1077 |
1076 |
1078 |
1077 |
1079 |
1078 (** balanced trees **) |
1080 (** balanced trees **) |
1079 |
1081 |