src/HOL/Algebra/Group.thy
 changeset 13949 0ce528cd6f19 parent 13944 9b34607cd83e child 13975 c8e9a89883ce
```     1.1 --- a/src/HOL/Algebra/Group.thy	Fri May 02 16:43:36 2003 +0200
1.2 +++ b/src/HOL/Algebra/Group.thy	Fri May 02 20:02:50 2003 +0200
1.3 @@ -6,14 +6,14 @@
1.4  Based on work by Florian Kammueller, L C Paulson and Markus Wenzel.
1.5  *)
1.6
1.7 -header {* Algebraic Structures up to Commutative Groups *}
1.9
1.10  theory Group = FuncSet:
1.11
1.12 -axclass number < type
1.13 +(* axclass number < type
1.14
1.15  instance nat :: number ..
1.16 -instance int :: number ..
1.17 +instance int :: number .. *)
1.18
1.19  section {* From Magmas to Groups *}
1.20
1.21 @@ -416,12 +416,7 @@
1.22      and m_inv_closed [intro, simp]: "x \<in> H ==> inv x \<in> H"
1.23
1.24  declare (in subgroup) group.intro [intro]
1.25 -(*
1.26 -lemma (in subgroup) l_oneI [intro]:
1.27 -  includes l_one G
1.28 -  shows "l_one (G(| carrier := H |))"
1.29 -  by rule simp_all
1.30 -*)
1.31 +
1.32  lemma (in subgroup) group_axiomsI [intro]:
1.33    includes group G
1.34    shows "group_axioms (G(| carrier := H |))"
1.35 @@ -511,15 +506,6 @@
1.36    "G \<times>\<^sub>g H == (| carrier = carrier (G \<times>\<^sub>s H),
1.37      mult = mult (G \<times>\<^sub>s H),
1.38      one = (one G, one H) |)"
1.39 -(*
1.40 -  DirProdGroup ::
1.41 -    "[('a, 'm) group_scheme, ('b, 'n) group_scheme] => ('a \<times> 'b) group"
1.42 -    (infixr "\<times>\<^sub>g" 80)
1.43 -  "G \<times>\<^sub>g H == (| carrier = carrier (G \<times>\<^sub>m H),
1.44 -    mult = mult (G \<times>\<^sub>m H),
1.45 -    one = one (G \<times>\<^sub>m H),
1.46 -    m_inv = (%(g, h). (m_inv G g, m_inv H h)) |)"
1.47 -*)
1.48
1.49  lemma DirProdSemigroup_magma:
1.50    includes magma G + magma H
1.51 @@ -659,7 +645,7 @@
1.52    with x show ?thesis by simp
1.53  qed
1.54
1.55 -section {* Commutative Structures *}
1.56 +subsection {* Commutative Structures *}
1.57
1.58  text {*
1.59    Naming convention: multiplicative structures that are commutative
```