| author | wenzelm |
| Sun, 14 Mar 2021 21:41:28 +0100 | |
| changeset 73437 | 5614aab3f83e |
| 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 |