[isabelle-dev] HOL vs. HOL-Complex

[Brian Huffman]

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