TFL/usyntax.sml
changeset 3713 8a1f7d5b1eff
parent 3405 2cccd0e3e9ea
child 6498 1ebbe18fe236
equal deleted inserted replaced
3712:242546f35f8e 3713:8a1f7d5b1eff
   237 
   237 
   238 (* These others are almost never used *)
   238 (* These others are almost never used *)
   239 fun list_mk_imp(A,c) = itlist(fn a => fn tm => mk_imp{ant=a,conseq=tm}) A c;
   239 fun list_mk_imp(A,c) = itlist(fn a => fn tm => mk_imp{ant=a,conseq=tm}) A c;
   240 fun list_mk_forall(V,t) = itlist(fn v => fn b => mk_forall{Bvar=v, Body=b})V t;
   240 fun list_mk_forall(V,t) = itlist(fn v => fn b => mk_forall{Bvar=v, Body=b})V t;
   241 val list_mk_conj = end_itlist(fn c1 => fn tm => mk_conj{conj1=c1, conj2=tm})
   241 val list_mk_conj = end_itlist(fn c1 => fn tm => mk_conj{conj1=c1, conj2=tm})
   242 val list_mk_disj = end_itlist(fn d1 => fn tm => mk_disj{disj1=d1, disj2=tm})
       
   243 
   242 
   244 
   243 
   245 (* Need to reverse? *)
   244 (* Need to reverse? *)
   246 fun gen_all tm = list_mk_forall(term_frees tm, tm);
   245 fun gen_all tm = list_mk_forall(term_frees tm, tm);
   247 
   246