Lines Matching defs:os
203 ���!os (a:'a) as.
204 (LENGTH os = LENGTH (CONS a as)) ==>
205 (?(o':'b) os'. (LENGTH os' = LENGTH as) /\ (os = CONS o' os'))���),
211 THEN EXISTS_TAC ���os:'b list���
216 ���!os:'b list.
217 (LENGTH os = LENGTH ([]:'a list)) ==>
218 (os = [])���),
274 fun MAKE_LIST_CLEAN_VAR_THM free_vrs (x, os) =
293 val mk_obj_list = foldr (fn (a,os) => ���CONS ^a ^os���)
295 val os_tm = mk_obj_list os
301 val os' = foldr (fn (v,l) => (Term.variant (l @ free_vrs) v)::l)
302 [] os
303 val os'_tm = mk_obj_list os'
306 val os'_vr = #Bvar(dest_abs body2)
307 val exists_tm1 = beta_conv (mk_comb{Rator=body2, Rand=os'_tm})
309 exists_tm1 os'
377 (EVERY (map (fn ((x,os),sigma_thm) =>
378 let val n = length os in