Email Gateway (Aug 22 2022 at 19:31): Email Gateway (Aug 22 2022 at 19:31):From: mailing-list anonymous <mailing.list.anonymous@gmail.com>
Dear All,
I noticed that there may be at least two duplicate theorems in
Isabelle2019-RC0/HOL. However, of course, I cannot be certain if the
duplicates were provided intentionally. The only difference between the
theorems seems to be in the use of the abbreviation trivial_limit. However,
the theorems seem to be exactly identical, except for the names of the
schematic variables. In particular, Topological_Spaces.Lim_in_closed_set
seems to be equivalent to Elementary_Topology.Lim_in_closed_set and
Topological_Spaces.Lim_ident_at seems to be equivalent to
Elementary_Topology.netlimit_within. Also, if the use of duplicates is
intentional, I would like to understand what are the reasons behind this.
Thank you
Message: 2
Email Gateway (Aug 22 2022 at 19:31):From: Lawrence Paulson <lp15@cam.ac.uk>
There must be many such duplications. They arise when we try to reorganise these huge theory libraries, so thanks for your report. It should be possible to get rid of those great easily.
In many cases there are a number of names for the same theorem, but with a single proof. That’s for the sake of compatibility, but personally I prefer to get rid of those as well.
Larry Paulson
Email Gateway (Aug 22 2022 at 19:33):From: Makarius <makarius@sketis.net>
Dear Isabelle users,
the release cycle for Isabelle2019 will officially start in approx. one
month. An informal snapshot Isabelle2019-RC0 for experimentation is
already available here: https://isabelle.in.tum.de/website-Isabelle2019-RC0
I have already updated the website content, including ANNOUNCE and NEWS,
but a few things will still change. Some documentation also needs to
updated.
The blog entry
https://sketis.net/2019/release-candidates-for-isabelle2019 is
dynamically updated to follow the release process.
In the past few years, we have routinely seen very odd non-causalities:
people looking at the release only after its final publication. But
final really means final (i.e. immutable, without further changes), and
problem reports that come too late need to wait 8-10 month for the next
release.
When discussing observations about release candidates, please provide a
Subject: line that fits to the content, not just a clone of the
announcement.
Makarius
Last updated: Apr 19 2024 at 08:19 UTC