Re: [isabelle] Two lemmas about lists constructed from finite sets that I'd like Isabelle to provide



On Wed, 22 May 2013, Christoph LANGE wrote:

I should have said that I'm using the Isabelle2013 release version.

You shouldn't. On isabelle-users you always refer implicitly to the latest release without saying that explicitly. Only if you use an older (official) release you should say that.

In contrast, if you are testing Isabelle repository versions, you should discuss your observations on the isabelle-dev mailing list (including the all-important Mercurial changeset id), not on isabelle-users.


Is it right that as soon as I switch to Isabelle2014 or to the development version I will be able to remove this code?

Isabelle release cycles vary between 6-10 months, but the year has invariably 12 months. So the next one is likely to be Isabelle2013-1 before the end of 2013, not Isabelle2014.

When working profesionally and productively with Isabelle you normally use the latest official release. Only if you have a special situation, and some extra time to follow the ongoing development process quickly, you may consider testing repository versions instead (see above).

Note that repository snapshots between the releases become outdated more quickly than the stable stepping stones. It is particularly bad to "get stuck" on some old snapshot while the official releases have moved on 1 or 2 steps already.


	Makarius




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