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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and