Lines Matching defs:l2
589 (``((l1 + r1) + (l2 + r2) = (l1 + l2) + (r1 + r2):real) /\
591 (tm1 + (l2 + r2) = l2 + (tm1 + r2)) /\
594 (tm1 + (l2 + r2) = (tm1 + l2) + r2)``,
612 val l2_tm = ``l2:real``
639 val (l2,r2) = dest tm2
640 val v2 = rand l2
646 val th1 = INST [(l1,l1_tm), (l2,l2_tm),
663 val th1 = INST [(tm1,tm1_tm), (l2,l2_tm), (r2,r2_tm)] pth3
699 val (l2,r2) = dest tm2
700 val v2 = rand l2
704 val th1 = INST [(tm1,tm1_tm), (l2,l2_tm), (r2,r2_tm)] pth6
712 val th1 = INST [(tm1,tm1_tm), (l2,l2_tm), (r2,r2_tm)] pth3
1006 fun union l1 l2 = itlist insert l1 l2;
1043 fun add_ineq (i1 as Lineq(k1,ty1,l1,just1)) (i2 as Lineq(k2,ty2,l2,just2)) =
1045 val l = map2 (curry op+) l1 l2
1066 fun elim_var v (i1 as Lineq(k1,ty1,l1,just1)) (i2 as Lineq(k2,ty2,l2,just2)) =
1069 val c2 = el0 v l2
1093 fun allpairs f l1 l2 = itlist (union o C map l2 o f) l1 [];
1094 fun op_allpairs eq f l1 l2 = itlist ((op_union eq) o C map l2 o f) l1 [];