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 70019 095dce9892e8
parent 69895 6b03a8cf092d
child 70027 94494b92d8d0 
--- a/src/HOL/Algebra/Coset.thy	Sat Mar 30 15:37:27 2019 +0100
+++ b/src/HOL/Algebra/Coset.thy	Mon Apr 01 17:02:43 2019 +0100
@@ -1379,7 +1379,7 @@
   qed
 qed
 
-lemma (in group) normal_inter_subgroup:
+lemma (in group) normal_Int_subgroup:
   assumes "subgroup H G"
     and "N \<lhd> G"
   shows "(N\<inter>H) \<lhd> (G\<lparr>carrier := H\<rparr>)"
isabelle