[isabelle-dev] Reorganising Analysis

[Lawrence Paulson]

I’m afraid that I’m to blame for this. I ported a huge amount of material from HOL Light and here, as in many other cases, I had to put it somewhere.

The biggest theory in the HOL Light analysis library is nearly 37,000 lines long.

Larry

> On 5 Nov 2019, at 03:13, Fabian Immler <immler at in.tum.de> wrote:
> 
> Starlike is a huge (8000loc) conglomeration and it may well be that we don't need all of it in a "Basic Analysis" session.
> 
> In a first attempt to get a better overview what is in there and why, I split off a theory about line segments (c2465b429e6e).
> 
> Then there is a lot (>2000loc) of material about relative interior/frontiers, which is a concept defined for convex sets, so perhaps it fits better in Convex_Euclidean_Space or (given the size) a seperate theory.
> 
> For the rest of the theory I could not identify clear topics anymore - the part on affine dimension might be worth separating from the rest.
> I only know that "Starlike" is a misnomer: there is just one definition and three lemmas about starlike sets in this huge theory.