Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Homology/Homology_Groups.thy
changeset 80175 200107cdd3ac
parent 80101 2ff4cc7fa70a 
--- a/src/HOL/Homology/Homology_Groups.thy	Sun May 05 15:31:08 2024 +0100
+++ b/src/HOL/Homology/Homology_Groups.thy	Mon May 06 14:39:33 2024 +0100
@@ -770,11 +770,11 @@
         using a chain_boundary_chain_map singular_relcycle by blast
       have contf: "continuous_map (subtopology X S) (subtopology Y T) f"
         using assms
-        by (auto simp: continuous_map_in_subtopology topspace_subtopology
-            continuous_map_from_subtopology)
+        by (auto simp: continuous_map_in_subtopology continuous_map_from_subtopology)
       show ?thesis
         unfolding q using assms p1 a
-        by (simp add: cbm ceq contf hom_boundary_chain_boundary hom_induced_chain_map p1_eq sb sr)
+        by (simp add: cbm ceq contf hom_boundary_chain_boundary hom_induced_chain_map p1_eq sb sr
+                 del: of_nat_diff)
     next
       case False
       with assms show ?thesis
isabelle