[isabelle] Unfortunate duplicate name



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.