Re: [isabelle] list_all vs set membership



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

Larry

> On 14 Oct 2020, at 22:47, Jakub Kądziołka <kuba at kadziolka.net> 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.