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/Algebra/Coset.thy
changeset 82248 e8c96013ea8a
parent 81438 95c9af7483b1 
--- a/src/HOL/Algebra/Coset.thy	Wed Mar 05 18:28:57 2025 +0100
+++ b/src/HOL/Algebra/Coset.thy	Tue Mar 11 10:20:44 2025 +0100
@@ -673,7 +673,7 @@
   interpret group G by fact
   show ?thesis
   proof (intro equivI)
-    have "rcong H \<subseteq> carrier G \<times> carrier G"
+    show "rcong H \<subseteq> carrier G \<times> carrier G"
       by (auto simp add: r_congruent_def)
     thus "refl_on (carrier G) (rcong H)"
       by (auto simp add: r_congruent_def refl_on_def)
isabelle