Lines Matching defs:ys
146 val ys = map prove_eq xs
148 val thms = map snd ys
150 in (ys,last_def,last_pre) end;
157 val (ys,def,pre) = compile_all_aux tm
160 in (ys,def,pre) :: compile_each tms end
166 val (ys,_,_) = last xs
168 val ys = map (fn (n,th) => (n,UNABBREV_CODE_RULE th)) ys
169 in (ys,defs,pres) end
180 | append_lists (y::ys) = y @ append_lists ys
202 val ys = map (mk_ALIGNED o snd) (xs1 @ xs2)
204 in ys @ zs end