| author | paulson <lp15@cam.ac.uk> |
| Fri, 17 Feb 2023 13:48:42 +0000 | |
| changeset 77279 | c16d423c9cb1 |
| 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 |