Lines Matching defs:t2
51 val (opt, t1, t2) = args_equiv w
57 if (t' ~~ t2) then
60 ([(asl, ``WEAK_EQUIV ^t' ^t2``)], fn [thm'] => OE_TRANS thm thm')
108 let val (t1, t2) = args_sum tm;
110 and thm2 = c t2;
111 val (t1', t1'') = args_thm thm1 (* t1' = t1, t2' = t2 *)
112 and (t2', t2'') = args_thm thm2
114 if t1' ~~ t1'' andalso t2' ~~ t2'' then
115 ISPEC (mk_sum (t1', t2')) WEAK_EQUIV_REFL
118 (LIST_CONJ [thm2, STABLE_CONV t2', STABLE_CONV t2'']))
119 else if t2' ~~ t2'' then
120 ISPEC t2' (MATCH_MP WEAK_EQUIV_SUBST_SUM_R
125 thm2, STABLE_CONV t2', STABLE_CONV t2''])
129 let val (t1, t2) = args_par tm;
131 and thm2 = c t2
173 let val (t1, t2) = args_sum tm;
175 and thm2 = OE_SUBST thm t2;
176 val (t1', t1'') = args_thm thm1 (* t1' = t1, t2' = t2 *)
177 and (t2', t2'') = args_thm thm2
179 if (t1' ~~ t1'') andalso (t2' ~~ t2'') then
180 ISPEC (mk_sum (t1', t2')) WEAK_EQUIV_REFL
183 (LIST_CONJ [thm2, STABLE_CONV t2', STABLE_CONV t2'']))
184 else if (t2' ~~ t2'') then
185 ISPEC t2' (MATCH_MP WEAK_EQUIV_SUBST_SUM_R
190 thm2, STABLE_CONV t2', STABLE_CONV t2''])
195 let val (t1, t2) = args_par tm;
197 and thm2 = OE_SUBST thm t2
221 val (opt, t1, t2) = args_equiv w
227 if (t' ~~ t2) then
230 ([(asl, ``WEAK_EQUIV ^t' ^t2``)], fn [thm''] => OE_TRANS thm' thm'')