changeset 32960 69916a850301
parent 31754 b5260f5272a4
child 32989 c28279b29ff1
--- a/src/HOL/Algebra/Group.thy	Sat Oct 17 01:05:59 2009 +0200
+++ b/src/HOL/Algebra/Group.thy	Sat Oct 17 14:43:18 2009 +0200
@@ -785,16 +785,16 @@
       assume H: "H \<in> A"
       with L have subgroupH: "subgroup H G" by auto
       from subgroupH have groupH: "group (G (| carrier := H |))" (is "group ?H")
-	by (rule subgroup_imp_group)
+        by (rule subgroup_imp_group)
       from groupH have monoidH: "monoid ?H"
-	by (rule group.is_monoid)
+        by (rule group.is_monoid)
       from H have Int_subset: "?Int \<subseteq> H" by fastsimp
       then show "le ?L ?Int H" by simp
       fix H
       assume H: "H \<in> Lower ?L A"
       with L Int_subgroup show "le ?L H ?Int"
-	by (fastsimp simp: Lower_def intro: Inter_greatest)
+        by (fastsimp simp: Lower_def intro: Inter_greatest)
       show "A \<subseteq> carrier ?L" by (rule L)