Re: [isabelle] How to avoid x \<in> carrier G proofs

Hi Gerwin,

Am Samstag, den 11.12.2010, 23:02 +1100 schrieb Gerwin Klein:
> I don't quite see the point in such a branch, though. An additional
> major theorem like this should be a new AFP submission, based on the
> existing entry. It should be based on the released version of the
> archive and the released version of Isabelle, not on
> which is the development
> version and unstable, often changing daily based on the development
> version of Isabelle.
> From the sound of it, we'd be more than happy to accept a new
> submission with the development you're working on.

ok, that wasn’t fully clear to me (and I already violated that rule by
finishing the free-group-isomorphism result in this commit:, sorry for

So at least in this case, I’d like to continue basing my work on
Isabelle-devel and AFP-devel (otherwise I’d have to undo compatibility
changes and add all the auxiliary lemmas that went into HOL by now), but
I’ll not push my changes but rather put my repository somewhere and ask
the editors to review and merge once (and if) I’m done.

Should such a new theorem be submitted as a new AFP entry or as an
update of the existing FreeGroup entry?


Joachim Breitner
  e-Mail: mail at
  ICQ#: 74513189
  Jabber-ID: nomeata at

Attachment: signature.asc
Description: This is a digitally signed message part

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