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, at 15:23, Makariuswrote: > > 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/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
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 the development. Larry > On 16 Sep 2016, at 16:20, Johannes Hölzlwrote: > > 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. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
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 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, Makariuswrote: > > > > 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
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, Makariuswrote: > > 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/isabelle-dev