Lines Matching refs:comp
76 (!X A B C. arrow X A B /\ arrow X B C ==> arrow X A C) /\ (* comp *)
79 val [one, beta, beta', gamma, gamma', comp, arrow_plus] =
81 (combine (["one", "beta", "beta'", "gamma", "gamma'", "comp", "arrow_plus"],
100 REWRITE_TAC [transitive_def, comp]);
164 >> MATCH_MP_TAC comp
175 >> MATCH_MP_TAC comp
185 >> MATCH_MP_TAC comp
195 >> MATCH_MP_TAC comp
206 >> MATCH_MP_TAC comp
219 >> MATCH_MP_TAC comp
231 >> MATCH_MP_TAC comp
250 >- PROVE_TAC [comp]
324 REWRITE_TAC [comp]);
1426 >> IMP_RES_TAC comp);
1619 IMP_RES_TAC comp,