src/HOL/Algebra/Group.thy
changeset 28823 dcbef866c9e2
parent 27714 27b4d7c01f8b
child 29237 e90d9d51106b
     1.1 --- a/src/HOL/Algebra/Group.thy	Mon Nov 17 17:00:27 2008 +0100
     1.2 +++ b/src/HOL/Algebra/Group.thy	Mon Nov 17 17:00:55 2008 +0100
     1.3 @@ -6,7 +6,9 @@
     1.4  Based on work by Florian Kammueller, L C Paulson and Markus Wenzel.
     1.5  *)
     1.6  
     1.7 -theory Group imports FuncSet Lattice begin
     1.8 +theory Group
     1.9 +imports Lattice FuncSet
    1.10 +begin
    1.11  
    1.12  
    1.13  section {* Monoids and Groups *}
    1.14 @@ -280,7 +282,7 @@
    1.15    qed
    1.16    then have carrier_subset_Units: "carrier G <= Units G"
    1.17      by (unfold Units_def) fast
    1.18 -  show ?thesis by unfold_locales (auto simp: r_one m_assoc carrier_subset_Units)
    1.19 +  show ?thesis proof qed (auto simp: r_one m_assoc carrier_subset_Units)
    1.20  qed
    1.21  
    1.22  lemma (in monoid) group_l_invI:
    1.23 @@ -685,7 +687,7 @@
    1.24    assumes m_comm: "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==>
    1.25        x \<otimes> y = y \<otimes> x"
    1.26    shows "comm_group G"
    1.27 -  by unfold_locales (simp_all add: m_comm)
    1.28 +  proof qed (simp_all add: m_comm)
    1.29  
    1.30  lemma comm_groupI:
    1.31    fixes G (structure)
    1.32 @@ -713,7 +715,7 @@
    1.33  
    1.34  theorem (in group) subgroups_partial_order:
    1.35    "partial_order (| carrier = {H. subgroup H G}, eq = op =, le = op \<subseteq> |)"
    1.36 -  by unfold_locales simp_all
    1.37 +  proof qed simp_all
    1.38  
    1.39  lemma (in group) subgroup_self:
    1.40    "subgroup (carrier G) G"