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 <[email protected]> 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. _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
