Re: [isabelle] Isabelle2019-RC0 available for experimentation



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


> On 5 Apr 2019, at 12:44, mailing-list anonymous <mailing.list.anonymous at gmail.com> wrote:
> 
> 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.
> 





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