Lines Matching defs:t1
23 (* Define S_SYM such that, when given a theorem A |- STRONG_EQUIV t1 t2,
24 returns the theorem A |- STRONG_EQUIV t2 t1. *)
56 val (opt, t1, t2) = args_equiv w
60 val thm = c t1
61 val (t1', t') = args_thm thm (* t1' = t1 *)
76 val (opt, t1, t2) = args_equiv w
82 if t'' ~~ t1 then ([], fn _ => S_SYM thm)
84 ([(asl, ``STRONG_EQUIV ^t1 ^t''``)],
106 let val (t1, t2) = args_sum tm;
107 val thm1 = c t1
113 let val (t1, t2) = args_par tm;
114 val thm1 = c t1
155 let val (t1, t2) = args_sum tm;
156 val thm1 = S_SUBST thm t1
162 let val (t1, t2) = args_par tm;
163 val thm1 = S_SUBST thm t1
188 val (opt, t1, t2) = args_equiv w
191 let val thm' = S_SUBST thm t1;
192 val (t1', t') = args_thm thm' (* t1' = t1 *)