Re: [isabelle] One more lemma to add to Isabelle/ZF

Victor Porton wrote:
I suggest one more lemma to add to Isabelle/ZF:

Dear Victor,

when I said "contributions are welcome", this was not an
invitation to spam this list with spontaneous proposals of trivial
lemmas, some of which you haven't even proved! Please stop doing
this, as it is just a waste of everybody's time!

Instead, my suggestion is this:

1. Learn the basics of Isabelle using the available documentation. Since
ZF has less documentation than HOL, it may be helpful to work through
the Isabelle/HOL tutorial first. Many things described there also apply
to ZF. Typically, getting sufficiently comfortable with the system to do
actual work takes a few months.

2. When you have mastered the basics, start working on some
formalization that you are interested in.

3. When you have proved something non-trivial, you can consider
submitting your formalization to the AFP (
Submissions will be reviewed by the editors and added to the AFP if
considered relevant. If in this process, it is discovered that some
lemmas should rather go directly into ZF, rather than the AFP, this will
be taken care of by the Isabelle developers.


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