Lines Matching defs:ps
379 val (ps,t) = ``(k:string |-> string list # term) ' ^name_tm``
382 val args = ps |> listSyntax.dest_list |> fst |> map stringSyntax.fromHOLstring
443 val (ps,t) = ``(k:string |-> string list # term) ' ^name_tm``
446 val args = ps |> listSyntax.dest_list |> fst |> map stringSyntax.fromHOLstring
491 val ps = params xs input_ty
492 val lhs = map (fn x => mk_comb(new_fun,x)) ps
498 val ss = map make_subs (zip data (zip ps lhs))
514 val ind_hyp_tm = map (fn (x,y) => mk_eq(mk_comb(mk_comb(new_prop,extra),x),y)) (zip ps aps)
528 |> CONV_RULE (RAND_CONV (ONCE_REWRITE_CONV [GSYM R_ap_SET_ENV]))) ps)
711 val (ps,t) = ``(k:string |-> string list # term) ' ^name_tm``
714 val args = ps |> listSyntax.dest_list |> fst |> map stringSyntax.fromHOLstring
736 SPECL [name_tm,ps,args,t] R_ap_NOT_OK
874 val ps = map parts defs_inds
875 val xs = ps |> map (fn (name,params,def,ind,body,rw,x1) => x1)
885 val (name,params,def,ind,body,rw,x1) = el 1 ps
889 val (ps,t) = ``(k:string |-> string list # term) ' ^name_tm``
892 val args = ps |> listSyntax.dest_list |> fst |> map stringSyntax.fromHOLstring
940 val thms = map prove_corr ps