summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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