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"