Quoting Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>:
> There is no urgent need that the HOL image contains *all* the > HOL-Complex theories. I also have been thinking about splitting off all > the Analysis stuff into a session HOL-Analysis, but on the other hand a > lot of functions which you naively expect for reals/complexes (log, ...) > inherently depend on analysis, as far as I understand. > > Florian If we all agree that reals and complexes really belong in the main HOL image, then that is a good reason for merging some of HOL-Complex into HOL. I also agree that not *all* of HOL-Complex needs to be in there. A good piece to split off would be all of the nonstandard-analysis stuff. Nothing else in HOL-Complex relies on any of the theories below (except that Complex_Main currently imports CLim and Hyperreal, which pulls in everything else). Infinite_Set, Zorn, Filter, StarDef, HyperNat, HyperDef, NSA, Star, HLim, NatStar, HSEQ, HDeriv, HSeries, HTranscendental, NSComplex, NSCA, HLog, Hyperreal, CStar, CLim It might make sense to split off some other stuff as well, but this would be a good start. If there are no objections, I could go ahead and split these theories myself. A good name might be HOL-NSA (for Non-Standard Analysis). Let me know what you think. - Brian
