[isabelle-dev] More HOL-Analysis

Lawrence Paulson lp15 at cam.ac.uk
Wed Sep 21 16:29:45 CEST 2016

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.


> On 16 Sep 2016, at 16:20, Johannes Hölzl <hoelzl at 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.

More information about the isabelle-dev mailing list