[isabelle-dev] HOL vs. HOL-Complex
brianh at cs.pdx.edu
Wed Jul 2 17:20:41 CEST 2008
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.
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.
More information about the isabelle-dev