Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Updating AFP entry


view this post on Zulip Email Gateway (Jan 11 2021 at 18:15):

From: Pedro Sánchez Terraf <sterraf@famaf.unc.edu.ar>
Hi all,

I've noted that I could make some small adjustment to an AFP entry of
mine that would make the transition to Isabelle2021 easier (one line vs
several replacements). Should I submit an update, or should I wait until
the AFP mantainers take care of it?

I would also take the chance to correct the name of a lemma!

view this post on Zulip Email Gateway (Jan 12 2021 at 07:36):

From: Tobias Nipkow <nipkow@in.tum.de>
On 11/01/2021 19:14, Pedro Sánchez Terraf wrote:

Hi all,

I've noted that I could make some small adjustment to an AFP entry of mine that
would make the transition to Isabelle2021 easier (one line vs several
replacements). Should I submit an update, or should I wait until the AFP
mantainers take care of it?

I would also take the chance to correct the name of a lemma!

I assume we are talking about an entry that is in the release version of the AFP
but not yet in the development version, probably Cofinality and the Delta System
Lemma? In that case you cannot change it because entries in the release version
are frozen. Once we move it over to the development version, it sounds like it
will need adjustment. In that case we (the AFP editors) may leave that work to
you - you should get an email from the system that your AFP entry did not build.

Tobias

--
Pedro Sánchez Terraf
CIEM-FAMAF — Universidad Nacional de Córdoba
cs.famaf.unc.edu.ar/~pedro/home_en
<https://cs.famaf.unc.edu.ar/~pedro/home_en.html>
smime.p7s

view this post on Zulip Email Gateway (Jan 12 2021 at 23:27):

From: Gerwin Klein <kleing@unsw.edu.au>
I have now merged these into the development version, so they should be available for updating there.

Cheers,
Gerwin
signature.asc


Last updated: Sep 25 2021 at 09:17 UTC