Re: [isabelle] Unfortunate duplicate name



The first one could/should be called Inf_eq_Sup.

Tobias

On 25/10/2019 18:48, 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})



Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



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