# HG changeset patch
# User wenzelm
# Date 1320680354 -3600
# Node ID 121b2db078b1ab68ff674185919a812e24b532ec
# Parent  7c1375ba142478742c4049eb3fe912689eaf5691
tuned proofs;

diff -r 7c1375ba1424 -r 121b2db078b1 src/HOL/Algebra/AbelCoset.thy
--- a/src/HOL/Algebra/AbelCoset.thy	Mon Nov 07 14:59:58 2011 +0100
+++ b/src/HOL/Algebra/AbelCoset.thy	Mon Nov 07 16:39:14 2011 +0100
@@ -246,21 +246,19 @@
   shows "abelian_subgroup H G"
 proof -
   interpret comm_group "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
-  by (rule a_comm_group)
+    by (rule a_comm_group)
   interpret subgroup "H" "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
-  by (rule a_subgroup)
+    by (rule a_subgroup)
 
   show "abelian_subgroup H G"
-  apply unfold_locales
+    apply unfold_locales
   proof (simp add: r_coset_def l_coset_def, clarsimp)
     fix x
     assume xcarr: "x \<in> carrier G"
-    from a_subgroup
-        have Hcarr: "H \<subseteq> carrier G" by (unfold subgroup_def, simp)
-    from xcarr Hcarr
-        show "(\<Union>h\<in>H. {h \<oplus>\<^bsub>G\<^esub> x}) = (\<Union>h\<in>H. {x \<oplus>\<^bsub>G\<^esub> h})"
-        using m_comm[simplified]
-        by fast
+    from a_subgroup have Hcarr: "H \<subseteq> carrier G"
+      unfolding subgroup_def by simp
+    from xcarr Hcarr show "(\<Union>h\<in>H. {h \<oplus>\<^bsub>G\<^esub> x}) = (\<Union>h\<in>H. {x \<oplus>\<^bsub>G\<^esub> h})"
+      using m_comm [simplified] by fast
   qed
 qed
 
@@ -543,9 +541,10 @@
 proof -
   interpret G: abelian_group G by fact
   interpret H: abelian_group H by fact
-  show ?thesis apply (intro abelian_group_hom.intro abelian_group_hom_axioms.intro)
-    apply fact
-    apply fact
+  show ?thesis
+    apply (intro abelian_group_hom.intro abelian_group_hom_axioms.intro)
+      apply fact
+     apply fact
     apply (rule a_group_hom)
     done
 qed