src/HOL/Algebra/Group.thy
 changeset 31754 b5260f5272a4 parent 31727 2621a957d417 child 32960 69916a850301 child 32988 d1d4d7a08a66
```     1.1 --- a/src/HOL/Algebra/Group.thy	Mon Jun 22 08:17:52 2009 +0200
1.2 +++ b/src/HOL/Algebra/Group.thy	Mon Jun 22 20:59:12 2009 +0200
1.3 @@ -542,10 +542,8 @@
1.4        (\<forall>x \<in> carrier G. \<forall>y \<in> carrier G. h (x \<otimes>\<^bsub>G\<^esub> y) = h x \<otimes>\<^bsub>H\<^esub> h y)}"
1.5
1.6  lemma (in group) hom_compose:
1.7 -     "[|h \<in> hom G H; i \<in> hom H I|] ==> compose (carrier G) i h \<in> hom G I"
1.8 -apply (auto simp add: hom_def funcset_compose)
1.9 -apply (simp add: compose_def Pi_def)
1.10 -done
1.11 +  "[|h \<in> hom G H; i \<in> hom H I|] ==> compose (carrier G) i h \<in> hom G I"
1.12 +by (fastsimp simp add: hom_def compose_def)
1.13
1.14  constdefs
1.15    iso :: "_ => _ => ('a => 'b) set"  (infixr "\<cong>" 60)
1.16 @@ -568,7 +566,7 @@
1.17
1.18  lemma DirProd_commute_iso:
1.19    shows "(\<lambda>(x,y). (y,x)) \<in> (G \<times>\<times> H) \<cong> (H \<times>\<times> G)"
1.20 -by (auto simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def)
1.21 +by (auto simp add: iso_def hom_def inj_on_def bij_betw_def)
1.22
1.23  lemma DirProd_assoc_iso:
1.24    shows "(\<lambda>(x,y,z). (x,(y,z))) \<in> (G \<times>\<times> H \<times>\<times> I) \<cong> (G \<times>\<times> (H \<times>\<times> I))"
1.25 @@ -592,7 +590,7 @@
1.26    "x \<in> carrier G ==> h x \<in> carrier H"
1.27  proof -
1.28    assume "x \<in> carrier G"
1.29 -  with homh [unfolded hom_def] show ?thesis by (auto simp add: Pi_def)
1.30 +  with homh [unfolded hom_def] show ?thesis by auto
1.31  qed
1.32
1.33  lemma (in group_hom) one_closed [simp]:
```