[isabelle-dev] \mu and \nu in HOL-Algebra [was Re: Towards the Isabelle2017 release]

[Clemens Ballarin]

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