| author | wenzelm | 
| Wed, 23 Mar 2022 12:21:13 +0100 | |
| changeset 75311 | 5960bae73afe | 
| 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: 
70095diff
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 |