src/HOL/Algebra/Group.thy
 changeset 35416 d8d7d1b785af parent 33057 764547b68538 child 35847 19f1f7066917
```     1.1 --- a/src/HOL/Algebra/Group.thy	Wed Feb 24 11:55:52 2010 +0100
1.2 +++ b/src/HOL/Algebra/Group.thy	Mon Mar 01 13:40:23 2010 +0100
1.3 @@ -478,8 +478,7 @@
1.4
1.5  subsection {* Direct Products *}
1.6
1.7 -constdefs
1.8 -  DirProd :: "_ \<Rightarrow> _ \<Rightarrow> ('a \<times> 'b) monoid"  (infixr "\<times>\<times>" 80)
1.9 +definition DirProd :: "_ \<Rightarrow> _ \<Rightarrow> ('a \<times> 'b) monoid" (infixr "\<times>\<times>" 80) where
1.10    "G \<times>\<times> H \<equiv> \<lparr>carrier = carrier G \<times> carrier H,
1.11                  mult = (\<lambda>(g, h) (g', h'). (g \<otimes>\<^bsub>G\<^esub> g', h \<otimes>\<^bsub>H\<^esub> h')),
1.12                  one = (\<one>\<^bsub>G\<^esub>, \<one>\<^bsub>H\<^esub>)\<rparr>"
1.13 @@ -545,8 +544,7 @@
1.14    "[|h \<in> hom G H; i \<in> hom H I|] ==> compose (carrier G) i h \<in> hom G I"
1.15  by (fastsimp simp add: hom_def compose_def)
1.16
1.17 -constdefs
1.18 -  iso :: "_ => _ => ('a => 'b) set"  (infixr "\<cong>" 60)
1.19 +definition iso :: "_ => _ => ('a => 'b) set" (infixr "\<cong>" 60) where
1.20    "G \<cong> H == {h. h \<in> hom G H & bij_betw h (carrier G) (carrier H)}"
1.21
1.22  lemma iso_refl: "(%x. x) \<in> G \<cong> G"
```