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 30240 5b25fee0362c
parent 29237 e90d9d51106b
child 31727 2621a957d417 
--- a/src/HOL/Algebra/Coset.thy	Wed Mar 04 10:43:39 2009 +0100
+++ b/src/HOL/Algebra/Coset.thy	Wed Mar 04 10:45:52 2009 +0100
@@ -602,8 +602,8 @@
   interpret group G by fact
   show ?thesis
   proof (intro equiv.intro)
-    show "refl (carrier G) (rcong H)"
-      by (auto simp add: r_congruent_def refl_def) 
+    show "refl_on (carrier G) (rcong H)"
+      by (auto simp add: r_congruent_def refl_on_def) 
   next
     show "sym (rcong H)"
     proof (simp add: r_congruent_def sym_def, clarify)
isabelle