--- a/src/HOL/Algebra/Group.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Algebra/Group.thy Mon Sep 12 07:55:43 2011 +0200
@@ -549,7 +549,7 @@
lemma (in group) hom_compose:
"[|h \<in> hom G H; i \<in> hom H I|] ==> compose (carrier G) i h \<in> hom G I"
-by (fastsimp simp add: hom_def compose_def)
+by (fastforce simp add: hom_def compose_def)
definition
iso :: "_ => _ => ('a => 'b) set" (infixr "\<cong>" 60)
@@ -781,7 +781,7 @@
fix A
assume L: "A \<subseteq> carrier ?L" and non_empty: "A ~= {}"
then have Int_subgroup: "subgroup (\<Inter>A) G"
- by (fastsimp intro: subgroups_Inter)
+ by (fastforce intro: subgroups_Inter)
show "\<exists>I. greatest ?L I (Lower ?L A)"
proof
show "greatest ?L (\<Inter>A) (Lower ?L A)"
@@ -794,13 +794,13 @@
by (rule subgroup_imp_group)
from groupH have monoidH: "monoid ?H"
by (rule group.is_monoid)
- from H have Int_subset: "?Int \<subseteq> H" by fastsimp
+ from H have Int_subset: "?Int \<subseteq> H" by fastforce
then show "le ?L ?Int H" by simp
next
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 (fastforce simp: Lower_def intro: Inter_greatest)
next
show "A \<subseteq> carrier ?L" by (rule L)
next