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 Freitag, den 16.09.2016, 15:43 +0100 schrieb Lawrence Paulson: > 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 <makar...@sketis.net> wrote: > > > > 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. > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabel > le-dev _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev