[isabelle-dev] NEWS

[Lawrence Paulson]

* Session HOL-Homology: New, a port of HOL Light's homology library,
with new proofs of "invariance of domain" and related results.

* Session HOL-Analysis: Better organization and much more material
at the level of abstract topological spaces.

* Session HOL-Algebra: Much more material on group theory, mostly ported
from HOL Light.

Note: we now have a big overlap with Analysis/Further_Topology, with many identical proofs of the consequences of invariance of domain. They can’t trivially be deleted, since Homology and Analysis are separate. In HOL Light’s analysis library, the homology development is loaded early. We’ll need to fix this somehow.

Larry