Lines Matching defs:lhs
404 val lhs = foldl (fn (x,y) => mk_comb(y,x)) new_fun params
408 val tm = mk_abs(args_var,subst (mk_els params args_var) lhs)
411 val def_tm = mk_eq(lhs,rhs)
492 val lhs = map (fn x => mk_comb(new_fun,x)) ps
498 val ss = map make_subs (zip data (zip ps lhs))
502 val def_tm = list_mk_conj (map mk_eq (zip lhs rhs))
746 val lhs = foldl (fn (x,y) => mk_comb(y,x)) new_fun params
751 val tm = pairSyntax.mk_pabs(vars,subst (mk_els params1 args_var) lhs)
754 val def_tm = mk_eq(lhs,rhs)
774 val lhs = mk_conj(hd (hyp (get_lookup_thm())),side_const_tm_full)
775 val goal = mk_imp(lhs,th7 |> concl |> rand)
914 val lhs = foldl (fn (x,y) => mk_comb(y,x)) new_fun params
918 val tm = mk_abs(args_var,subst (mk_els params args_var) lhs)