src/HOL/Algebra/Group.thy
changeset 61169 4de9ff3ea29a
parent 58622 aa99568f56de
child 61382 efac889fccbc
     1.1 --- a/src/HOL/Algebra/Group.thy	Sun Sep 13 22:25:21 2015 +0200
     1.2 +++ b/src/HOL/Algebra/Group.thy	Sun Sep 13 22:56:52 2015 +0200
     1.3 @@ -286,7 +286,8 @@
     1.4    qed
     1.5    then have carrier_subset_Units: "carrier G <= Units G"
     1.6      by (unfold Units_def) fast
     1.7 -  show ?thesis by default (auto simp: r_one m_assoc carrier_subset_Units)
     1.8 +  show ?thesis
     1.9 +    by standard (auto simp: r_one m_assoc carrier_subset_Units)
    1.10  qed
    1.11  
    1.12  lemma (in monoid) group_l_invI:
    1.13 @@ -730,7 +731,7 @@
    1.14    assumes m_comm: "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==>
    1.15        x \<otimes> y = y \<otimes> x"
    1.16    shows "comm_group G"
    1.17 -  by default (simp_all add: m_comm)
    1.18 +  by standard (simp_all add: m_comm)
    1.19  
    1.20  lemma comm_groupI:
    1.21    fixes G (structure)
    1.22 @@ -758,7 +759,7 @@
    1.23  
    1.24  theorem (in group) subgroups_partial_order:
    1.25    "partial_order \<lparr>carrier = {H. subgroup H G}, eq = op =, le = op \<subseteq>\<rparr>"
    1.26 -  by default simp_all
    1.27 +  by standard simp_all
    1.28  
    1.29  lemma (in group) subgroup_self:
    1.30    "subgroup (carrier G) G"