* 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 _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
