author | wenzelm |
Tue, 03 Dec 2019 16:40:04 +0100 | |
changeset 71222 | 2bc39c80a95d |
parent 70113 | c8deb8ba6d05 |
permissions | -rw-r--r-- |
70089
eca8611201e9
new Homology target, depending on HOL-Algebra and HOL-Analysis
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1 |
theory Homology |
70113
c8deb8ba6d05
Fixing the main Homology theory; also moving a lot of sum/prod lemmas into their generic context
paulson <lp15@cam.ac.uk>
parents:
70095
diff
changeset
|
2 |
imports Invariance_of_Domain |
70089
eca8611201e9
new Homology target, depending on HOL-Algebra and HOL-Analysis
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
3 |
begin |
eca8611201e9
new Homology target, depending on HOL-Algebra and HOL-Analysis
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
4 |
|
eca8611201e9
new Homology target, depending on HOL-Algebra and HOL-Analysis
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
5 |
end |