Lines Matching defs:t4
173 val t4 = list_mk_forall (args, t3)
175 t4
183 val t4 = list_mk_forall ([input_arg, input_arg']@(List.map snd case_args)@(List.map snd case_args'), t3)
187 val thm0 = HO_REWR_CONV forall_thm t4
216 val t4 = list_mk_forall ([input_arg, const]@consts, t3)
220 val thm0 = HO_REWR_CONV forall_thm t4
251 val t4 = mk_eq (t3a, t3b)
253 val t5 = list_mk_forall ([input_arg, const]@consts, t4)
288 val t4 = list_mk_forall ([input_arg, const]@consts, t3)
292 val thm0 = HO_REWR_CONV forall_thm t4