There seems to be an ongoing consolidation of HOL-Analysis (although the
NEWS are relatively terse about it).
How about moving src/HOL/Library/Continuum_Not_Denumerable.thy there,
too? The recent change b746b19197bd appears to supports this.
There might be more Analysis material in HOL-Library th
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 about it).
>
> How about
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 F
