Lines Matching defs:c2
55 val (c1, c2) = dest_conj tm
63 K (SPEC c2 T_and_l)
65 K (SPEC c2 F_and_l)
68 SOME (DISCH c1 (REWRITE_CONV [EQT_INTRO (ASSUME c1)] c2))
184 val (c1,c2) = dest_conj tm
381 val c2 = sum_var_coeffs v arg2
384 if c1 = c2 then (zero,zero)
387 if Arbint.<(c1, c2) then (one,zero) else (zero,one)
389 if Arbint.<(c1, c2) then (zero,one) else (one,zero)
536 c1 | ... /\ c2 | ...