Re: [isabelle-dev] More HOL-Analysis

Please let me know when you move the file Continuum_Not_Denumerable.thy. I have quite a few theorems connected with cardinality and topological concepts. Possibly they should not be added to that theory and it should simply be included at some point in the development. Larry > On 16 Sep 2016,

Re: [isabelle-dev] More HOL-Analysis

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

Re: [isabelle-dev] More HOL-Analysis

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.  - Johannes Am

Re: [isabelle-dev] More HOL-Analysis

I’m continuing to port a lot of material from HOL Light, and indeed I’m going to need that exact theory very soon. Larry > On 16 Sep 2016, at 15:23, Makarius wrote: > > There seems to be an ongoing consolidation of HOL-Analysis (although the > NEWS are relatively terse