Convex_Euclidean_Space is the largest file in Analysis, more than half a megabyte, so rather than combining the files it would be good to split them up even more.
I admit, I have been putting in a lot of new material and trying to put things in sensible places, but with no global overview of the development. Larry > On 16 Sep 2016, at 16:20, Johannes Hölzl <hoe...@in.tum.de> wrote: > > Also Brian's theories are still in HOL-Library (i.e. Inner_Product and > Product_Vector). I would also move Convex back. It was split of > Convex_Euclidean_Space to be usable in Probability. Which is not > necessary anymore as Probability is based on Analysis. > > I will move these files. _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev