equal
deleted
inserted
replaced
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 |