Re: [isabelle] Unfortunate duplicate name



I guess that I am responsible for introducing the second lemma, and there is also the dual version.

Probably changing Complete_Lattices.complete_distrib_lattice_class.Inf_Sup

to Complete_Lattices.complete_distrib_lattice_class.Inf_Sup_distrib

would be best as it would use the same pattern as inf_sup_distrib.

Viorel

On 10/25/2019 7:48 PM, Peter Lammich wrote:
Hi,

the second lemma named "Inf_Sup" hides the first one, making it only
accessible by its (tedious to write) long name. Can we rename one of
these lemmas?

--
   Peter

Complete_Lattices.complete_lattice_class.Inf_Sup: Inf ?A = Sup {b.
∀a∈?A. b ≤ a}
   Complete_Lattices.complete_distrib_lattice_class.Inf_Sup: Inf (Sup `
?A) = Sup (Inf ` {f ` ?A |f. ∀Y∈?A. f Y ∈ Y})






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