Lines Matching defs:ys
66 ``!xs b y ys. (str2sym_aux xs b = (y,ys)) ==> LENGTH ys <= LENGTH xs``,
72 \\ TRY (Q.PAT_X_ASSUM `zs = ys` (ASSUME_TAC)) \\ FULL_SIMP_TAC std_ss []
77 ``!xs y ys. (str2sym (x::xs) = (y,ys)) ==> LENGTH ys <= LENGTH xs``,
398 val ys = map (fn x => (x,genvar(type_of x))) xs
399 val tm2 = subst (map (fn (x,y) => x |-> y) ys) tm
401 in INST (map (fn (x,y) => y |-> x) ys) tm3 end
425 \\ Q.SPEC_TAC (`""`,`ys`) \\ Induct_on `xs`