Re: [isabelle] How to avoid x \<in> carrier G proofs
I'll leave the content questions to others on the list who know more about the formalisation.
To expand a bit on Alex's answer for the AFP question:
> PS: Is it ok to create personal branches, named appropriately, on
> http://afp.hg.sourceforge.net/hgweb/afp/afp/ where I could push my work
> to cite it here?
No, the AFP will not support branches, definitely not in-repository branches. As Alex said, this would be a maintenance nightmare, but it also does not make sense for what the AFP is -- a public archive of reviewed entries.
It may be a reasonable idea to use a branch locally for development, but publishing it for citing it separately and using the name AFP for it would be very much discouraged. The point of the AFP is that it is quality controlled and edited.
We give authors access to the development version of the AFP for maintenance, but we trust them to make maintenance changes only and we monitor all commits. Adding major developments is not what this access if for, much less adding new entries. Any such activities need to be coordinated with the editors.
Technically, to create a branch, you could make a local clone of the repository (not an in-repository branch) and work on that.
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 http://afp.hg.sourceforge.net/hgweb/afp/afp/ 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and