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.


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

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?


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.