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.
Clemens _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
