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"
```