Lines Matching defs:t1
51 val (opt, t1, t2) = args_equiv w
54 let val thm = MATCH_MP STRONG_IMP_WEAK_EQUIV (STRONG_EXP_THM_CONV t1);
55 val (t1', t') = args_thm thm (* t1' = t1 *)
108 let val (t1, t2) = args_sum tm;
109 val thm1 = c t1
111 val (t1', t1'') = args_thm thm1 (* t1' = t1, t2' = t2 *)
114 if t1' ~~ t1'' andalso t2' ~~ t2'' then
115 ISPEC (mk_sum (t1', t2')) WEAK_EQUIV_REFL
116 else if t1' ~~ t1'' then
117 ISPEC t1' (MATCH_MP WEAK_EQUIV_SUBST_SUM_L
121 (LIST_CONJ [thm1, STABLE_CONV t1', STABLE_CONV t1'']))
124 (LIST_CONJ [thm1, STABLE_CONV t1', STABLE_CONV t1'',
129 let val (t1, t2) = args_par tm;
130 val thm1 = c t1
173 let val (t1, t2) = args_sum tm;
174 val thm1 = OE_SUBST thm t1
176 val (t1', t1'') = args_thm thm1 (* t1' = t1, t2' = t2 *)
179 if (t1' ~~ t1'') andalso (t2' ~~ t2'') then
180 ISPEC (mk_sum (t1', t2')) WEAK_EQUIV_REFL
181 else if (t1' ~~ t1'') then
182 ISPEC t1' (MATCH_MP WEAK_EQUIV_SUBST_SUM_L
186 (LIST_CONJ [thm1, STABLE_CONV t1', STABLE_CONV t1'']))
189 (LIST_CONJ [thm1, STABLE_CONV t1', STABLE_CONV t1'',
195 let val (t1, t2) = args_par tm;
196 val thm1 = OE_SUBST thm t1
221 val (opt, t1, t2) = args_equiv w
224 let val thm' = OE_SUBST thm t1;
225 val (t1', t') = args_thm thm' (* t1' = t1 *)