src/HOL/Algebra/Group.thy
changeset 32960 69916a850301
parent 31754 b5260f5272a4
child 32989 c28279b29ff1
     1.1 --- a/src/HOL/Algebra/Group.thy	Sat Oct 17 01:05:59 2009 +0200
     1.2 +++ b/src/HOL/Algebra/Group.thy	Sat Oct 17 14:43:18 2009 +0200
     1.3 @@ -785,16 +785,16 @@
     1.4        assume H: "H \<in> A"
     1.5        with L have subgroupH: "subgroup H G" by auto
     1.6        from subgroupH have groupH: "group (G (| carrier := H |))" (is "group ?H")
     1.7 -	by (rule subgroup_imp_group)
     1.8 +        by (rule subgroup_imp_group)
     1.9        from groupH have monoidH: "monoid ?H"
    1.10 -	by (rule group.is_monoid)
    1.11 +        by (rule group.is_monoid)
    1.12        from H have Int_subset: "?Int \<subseteq> H" by fastsimp
    1.13        then show "le ?L ?Int H" by simp
    1.14      next
    1.15        fix H
    1.16        assume H: "H \<in> Lower ?L A"
    1.17        with L Int_subgroup show "le ?L H ?Int"
    1.18 -	by (fastsimp simp: Lower_def intro: Inter_greatest)
    1.19 +        by (fastsimp simp: Lower_def intro: Inter_greatest)
    1.20      next
    1.21        show "A \<subseteq> carrier ?L" by (rule L)
    1.22      next