From 3ab890c464256e343137abc270928cb3b461555c Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Thu, 8 Jun 2017 12:12:46 -0400 Subject: [PATCH] fix rename ordinary_theory -> ordinary_cohomology_theory --- homotopy/cohomology.hlean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/homotopy/cohomology.hlean b/homotopy/cohomology.hlean index 0317070..8c25b70 100644 --- a/homotopy/cohomology.hlean +++ b/homotopy/cohomology.hlean @@ -270,7 +270,7 @@ cohomology_theory.mk -- print has_choice_lift -- print equiv_lift -- print has_choice_equiv_closed -definition ordinary_cohomology_theory_EM [constructor] (G : AbGroup) : ordinary_theory := -⦃ordinary_theory, cohomology_theory_spectrum (EM_spectrum G), Hdimension := EM_dimension G ⦄ +definition ordinary_cohomology_theory_EM [constructor] (G : AbGroup) : ordinary_cohomology_theory := +⦃ordinary_cohomology_theory, cohomology_theory_spectrum (EM_spectrum G), Hdimension := EM_dimension G ⦄ end cohomology