src/HOL/Algebra/Group.thy
changeset 44890 22f665a2e91c
parent 44655 fe0365331566
child 46008 c296c75f4cf4
     1.1 --- a/src/HOL/Algebra/Group.thy	Sun Sep 11 22:56:05 2011 +0200
     1.2 +++ b/src/HOL/Algebra/Group.thy	Mon Sep 12 07:55:43 2011 +0200
     1.3 @@ -549,7 +549,7 @@
     1.4  
     1.5  lemma (in group) hom_compose:
     1.6    "[|h \<in> hom G H; i \<in> hom H I|] ==> compose (carrier G) i h \<in> hom G I"
     1.7 -by (fastsimp simp add: hom_def compose_def)
     1.8 +by (fastforce simp add: hom_def compose_def)
     1.9  
    1.10  definition
    1.11    iso :: "_ => _ => ('a => 'b) set" (infixr "\<cong>" 60)
    1.12 @@ -781,7 +781,7 @@
    1.13    fix A
    1.14    assume L: "A \<subseteq> carrier ?L" and non_empty: "A ~= {}"
    1.15    then have Int_subgroup: "subgroup (\<Inter>A) G"
    1.16 -    by (fastsimp intro: subgroups_Inter)
    1.17 +    by (fastforce intro: subgroups_Inter)
    1.18    show "\<exists>I. greatest ?L I (Lower ?L A)"
    1.19    proof
    1.20      show "greatest ?L (\<Inter>A) (Lower ?L A)"
    1.21 @@ -794,13 +794,13 @@
    1.22          by (rule subgroup_imp_group)
    1.23        from groupH have monoidH: "monoid ?H"
    1.24          by (rule group.is_monoid)
    1.25 -      from H have Int_subset: "?Int \<subseteq> H" by fastsimp
    1.26 +      from H have Int_subset: "?Int \<subseteq> H" by fastforce
    1.27        then show "le ?L ?Int H" by simp
    1.28      next
    1.29        fix H
    1.30        assume H: "H \<in> Lower ?L A"
    1.31        with L Int_subgroup show "le ?L H ?Int"
    1.32 -        by (fastsimp simp: Lower_def intro: Inter_greatest)
    1.33 +        by (fastforce simp: Lower_def intro: Inter_greatest)
    1.34      next
    1.35        show "A \<subseteq> carrier ?L" by (rule L)
    1.36      next