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


Am Sonntag, den 12.12.2010, 10:54 +1100 schrieb Gerwin Klein:
> Your description sounded like major new work to me, in size at least
> on the order of the existing entry. I would not say that this is just
> a small addition or maintenance change then. One indication for this
> was that you wanted to cite the change. 

ah, there is a misunderstanding, cause by unclear wording on my side.
With “cite” I meant that I want to show my current development state
easily when asking technical questions (which started this thread), and
it would be convenient to have it available in some publicly readable
repository with hgweb access. I did not mean or plan citing in the
academical sense.

(But I still see that with hg it is inconvenient to have personal
branches in the AFP repository and that I will host my branch somewhere

> So from a practical point of view, we should discuss off-list how big
> your change really is and if it should be merged or not. It's hard to
> say without seeing the new development or knowing more about it.

I’ll raise that once it’s ready.

> > 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.
> If that is what you want to do, a local hg clone of the afp
> development repository is probably the right way to go, because you
> can pull in Isabelle related changes.

yes, this is already what I’m doing.


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.