src/HOL/Homology/Homology.thy
author wenzelm
Thu, 10 Nov 2022 12:21:44 +0100
changeset 76504 15b058bb2416
parent 70113 c8deb8ba6d05
permissions -rw-r--r--
clarified signature: ensure that entries are well-formed --- no consecutive separators, no separators at start/end;
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