| author | haftmann | 
| Mon, 26 Oct 2020 11:28:43 +0000 | |
| changeset 72508 | c89d8e8bd8c7 | 
| 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 |