Re: [isabelle] Isabelle2019-RC0 available for experimentation



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
> Date: Tue, 2 Apr 2019 17:11:38 +0200
> From: Makarius <makarius at sketis.net>
> Subject: [isabelle] Isabelle2019-RC0 available for experimentation
> To: cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>
> Message-ID: <34e6702d-948f-a4cd-3621-b05984d54528 at sketis.net>
> Content-Type: text/plain; charset=utf-8
> 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



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