src/HOL/Algebra/Group.thy
 changeset 55926 3ef14caf5637 parent 55415 05f5fdb8d093 child 57271 3a20f8a24b13
     1.1 --- a/src/HOL/Algebra/Group.thy	Wed Mar 05 20:07:43 2014 +0100
1.2 +++ b/src/HOL/Algebra/Group.thy	Wed Mar 05 21:51:30 2014 +0100
1.3 @@ -721,7 +721,7 @@
1.4  text_raw {* \label{sec:subgroup-lattice} *}
1.5
1.6  theorem (in group) subgroups_partial_order:
1.7 -  "partial_order (| carrier = {H. subgroup H G}, eq = op =, le = op \<subseteq> |)"
1.8 +  "partial_order \<lparr>carrier = {H. subgroup H G}, eq = op =, le = op \<subseteq>\<rparr>"
1.9    by default simp_all
1.10
1.11  lemma (in group) subgroup_self:
1.12 @@ -729,7 +729,7 @@
1.13    by (rule subgroupI) auto
1.14
1.15  lemma (in group) subgroup_imp_group:
1.16 -  "subgroup H G ==> group (G(| carrier := H |))"
1.17 +  "subgroup H G ==> group (G\<lparr>carrier := H\<rparr>)"
1.18    by (erule subgroup.subgroup_is_group) (rule group_axioms)
1.19
1.20  lemma (in group) is_monoid [intro, simp]:
1.21 @@ -737,7 +737,7 @@
1.22    by (auto intro: monoid.intro m_assoc)
1.23
1.24  lemma (in group) subgroup_inv_equality:
1.25 -  "[| subgroup H G; x \<in> H |] ==> m_inv (G (| carrier := H |)) x = inv x"
1.26 +  "[| subgroup H G; x \<in> H |] ==> m_inv (G \<lparr>carrier := H\<rparr>) x = inv x"
1.27  apply (rule_tac inv_equality [THEN sym])
1.28    apply (rule group.l_inv [OF subgroup_imp_group, simplified], assumption+)
1.29   apply (rule subsetD [OF subgroup.subset], assumption+)
1.30 @@ -766,7 +766,7 @@
1.31  qed
1.32
1.33  theorem (in group) subgroups_complete_lattice:
1.34 -  "complete_lattice (| carrier = {H. subgroup H G}, eq = op =, le = op \<subseteq> |)"
1.35 +  "complete_lattice \<lparr>carrier = {H. subgroup H G}, eq = op =, le = op \<subseteq>\<rparr>"
1.36      (is "complete_lattice ?L")
1.37  proof (rule partial_order.complete_lattice_criterion1)
1.38    show "partial_order ?L" by (rule subgroups_partial_order)
1.39 @@ -784,7 +784,7 @@
1.40      fix H
1.41      assume H: "H \<in> A"
1.42      with L have subgroupH: "subgroup H G" by auto
1.43 -    from subgroupH have groupH: "group (G (| carrier := H |))" (is "group ?H")
1.44 +    from subgroupH have groupH: "group (G \<lparr>carrier := H\<rparr>)" (is "group ?H")
1.45        by (rule subgroup_imp_group)
1.46      from groupH have monoidH: "monoid ?H"
1.47        by (rule group.is_monoid)