[isabelle-dev] \mu and \nu in HOL-Algebra [was Re: Towards the Isabelle2017 release]
Clemens Ballarin
ballarin at in.tum.de
Fri Sep 1 10:25:10 CEST 2017
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
More information about the isabelle-dev
mailing list