I'm still working on integrating your HOL Light measure theory with HOL-Analysis. Showing that HK-integrable implies measurable is more involved as I though.
When this is finished I will move the theories. I'm not sure yet what to do with Convex and Convex_Euclidean_Spaces. - Johannes Am Mittwoch, den 21.09.2016, 17:03 +0100 schrieb Lawrence Paulson: > 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, 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. > > > > There might be more Analysis material in HOL-Library that is worth > > moving. > > > > > > Makarius > > _______________________________________________ > > isabelle-dev mailing list > > isabelle-...@in.tum.de > > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isab > > elle-dev > _______________________________________________ > 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