On 2017-08-31 13:54, Florian Haftmann wrote:
The theorem in question requires both the notion of subgroup and
complete lattices, hence the import order dictates in which theory the
theorem has to reside (btw. the current import order is similar to
HOL-Main where Complete_Lattices comes after Groups).
The theorem in question is that of the subgroups of a group forming a
complete lattice. Such theorems exist for many algebraic structures.
Following your approach they would all end up in Complete_Lattice,
making that a very big theory. I had decided against that.
isabelle-dev mailing list