--- a/src/HOL/Algebra/Group.thy Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/Algebra/Group.thy Mon Nov 17 17:00:55 2008 +0100
@@ -6,7 +6,9 @@
Based on work by Florian Kammueller, L C Paulson and Markus Wenzel.
*)
-theory Group imports FuncSet Lattice begin
+theory Group
+imports Lattice FuncSet
+begin
section {* Monoids and Groups *}
@@ -280,7 +282,7 @@
qed
then have carrier_subset_Units: "carrier G <= Units G"
by (unfold Units_def) fast
- show ?thesis by unfold_locales (auto simp: r_one m_assoc carrier_subset_Units)
+ show ?thesis proof qed (auto simp: r_one m_assoc carrier_subset_Units)
qed
lemma (in monoid) group_l_invI:
@@ -685,7 +687,7 @@
assumes m_comm: "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==>
x \<otimes> y = y \<otimes> x"
shows "comm_group G"
- by unfold_locales (simp_all add: m_comm)
+ proof qed (simp_all add: m_comm)
lemma comm_groupI:
fixes G (structure)
@@ -713,7 +715,7 @@
theorem (in group) subgroups_partial_order:
"partial_order (| carrier = {H. subgroup H G}, eq = op =, le = op \<subseteq> |)"
- by unfold_locales simp_all
+ proof qed simp_all
lemma (in group) subgroup_self:
"subgroup (carrier G) G"