src/HOL/Homology/Homology.thy
author wenzelm
Tue, 03 Dec 2019 16:40:04 +0100
changeset 71222 2bc39c80a95d
parent 70113 c8deb8ba6d05
permissions -rw-r--r--
clarified export of consts: recursion is accessible via spec_rules;
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