Lines Matching defs:l2
71 fun findMatches ([], l2) = []
72 | findMatches (a::l1, l2) =
74 val l2' = filter (fn e => not (eq_sym_aconv e a)) l2;
75 val l = (findMatches (l1',l2')); in
76 if eq_sym_mem a l2 then a::l else l end;
89 fun findMatches___multiple (l1:(term * bool) list,l2:(term * bool) list) =
90 map (fn t => (t, true)) (findMatches (map fst l1, map fst l2));
125 (let val (l1,l2) = get_impl_terms___multiple (dest_neg t) in
126 (map (fn (t,b) => (mk_neg___idempot t, b)) l2, map (fn (t,b) => (mk_neg___idempot t, b)) l1)
142 val (l1,l2) = get_impl_terms___multiple b;
145 ((t,false)::(filter filter_pred l1), (t,false)::(filter filter_pred l2))
162 val (l1,l2) = get_impl_terms___multiple t;
164 (map fst l1, map fst l2)