src/HOL/Homology/Homology.thy
author haftmann
Mon, 26 Oct 2020 11:28:43 +0000
changeset 72508 c89d8e8bd8c7
parent 70113 c8deb8ba6d05
permissions -rw-r--r--
factored out theory Traditional_Syntax
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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