Lines Matching defs:t1
68 val (t1, t2) = dest_disj t
70 if (aconv t1 T) then
73 SPEC t1 (ConseqConvTheory.OR_CLAUSES_XT)
75 val thm1_opt = SOME (ALL_DISJ_TF_ELIM_CONV c t1) handle UNCHANGED => NONE
89 val (t1', t2') = dest_disj (rhs (concl thm0))
91 val rewr_thm_opt = if (aconv t1' T) then
93 else if (aconv t1' F) then
232 val (t1, t2) = dest_comb t
233 val (t1', avoid1) = REMOVE_REBIND_CONV_AUX avoid t1
236 (mk_comb (t1', t2'), avoid2)
293 | Psyntax.COMB (t1, t2) => let
294 val (dups', seen') = MULTIPLE_FV_AUX dups seen t1
428 val t1 = mk_comb (b_tm, v)
429 val t2 = mk_comb (t1, rows)
729 val t1 = mk_comb (b_tm, v)
730 val t2 = mk_comb (t1, rows)