Re: [isabelle] list_all vs set membership

I would avoid the [iff] attribute, since users may not want to have list_all rewritten away.


> On 14 Oct 2020, at 22:47, Jakub Kądziołka <kuba at> wrote:
> lemma list_all_iff_forall_set [iff]:
>  "list_all P xs ⟷ (∀x. x ∈ set xs ⟶ P x)"

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.