author | haftmann |
Sun, 09 Feb 2020 10:46:32 +0000 | |
changeset 71424 | e83fe2c31088 |
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 |