Re: [isabelle] Unfortunate duplicate name

The first one could/should be called Inf_eq_Sup.


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

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

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