> Il giorno 07 gen 2019, alle ore 01:52, Waqar Ahmad <12phdwah...@seecs.edu.pk> > ha scritto: > > Hi Chun, > > I think it’s better to let HOL maintainers to decide if we should keep the > old version (14,700 lines) in “examples”, e.g. “examples/old-probability”. I > personally don’t like this idea, because the old version is always accessible > from previous HOL releases. And there’re still many redundant > probability-related scripts to be cleaned up from the example folder. > > Ideally, both these measures (real and extreal-valued) should be part of one > script as in Isabelle's measure theory. However, in our case, a fair argument > would be to put the efforts on the new measure theory since it has more > potential for future development compared to the old one. Since, the old > version can be easily accessible from HOL-releases I think there is no need > to drag it along. Please, go ahead and make this PR.
Where’re the measures of real and extreal-valued in Isabelle’s measure theory?
I only saw one version based on Extended Non-Negative Reals ('a set ⇒ ennreal)
in “src/HOL/Analysis/Measure_Space.thy)
—Chun
signature.asc
Description: Message signed with OpenPGP using GPGMail
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
