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)