[isabelle] More on foundation axiom
In ZF.thy the foundation axiom is:
foundation: "A=0 | (\<exists>x\<in>A. \<forall>y\<in>x. y~:A)"
Why there are no simplified version?
foundation: "A=0 | (\<exists>x\<in>A. x Int A=0)"
Isn't the latter more convenient in use?
So my question: Why there are no second version of foundation in Isabelle/ZF?
Victor Porton - http://portonvictor.org
This archive was generated by a fusion of
Pipermail (Mailman edition) and