Lines Matching defs:os
200 ���!os (a:'a) as.
201 (LENGTH os = LENGTH (CONS a as)) ==>
202 (?(o':'b) os'. (LENGTH os' = LENGTH as) /\ (os = CONS o' os'))���),
208 THEN EXISTS_TAC ���os:'b list���
213 ���!os:'b list.
214 (LENGTH os = LENGTH ([]:'a list)) ==>
215 (os = [])���),
265 fun MAKE_LIST_CLEAN_VAR_THM free_vrs (x, os) =
278 val mk_term_list = foldr (fn (a,os) => ���CONS ^a ^os���)
280 val os_tm = mk_term_list os
286 val os' = foldr (fn (v,l) => (Term.variant (l @ free_vrs) v)::l)
287 [] os
288 val os'_tm = mk_term_list os'
291 val os'_vr = #Bvar(dest_abs body2)
292 val exists_tm1 = beta_conv (mk_comb{Rator=body2, Rand=os'_tm})
294 exists_tm1 os'
362 (EVERY (map (fn ((x,os),lambda_thm) =>
363 let val n = length os in