--- a/src/HOL/Algebra/Group.thy Fri Sep 02 17:58:32 2011 +0200
+++ b/src/HOL/Algebra/Group.thy Fri Sep 02 18:17:45 2011 +0200
@@ -286,7 +286,7 @@
qed
then have carrier_subset_Units: "carrier G <= Units G"
by (unfold Units_def) fast
- show ?thesis proof qed (auto simp: r_one m_assoc carrier_subset_Units)
+ show ?thesis by default (auto simp: r_one m_assoc carrier_subset_Units)
qed
lemma (in monoid) group_l_invI:
@@ -694,7 +694,7 @@
assumes m_comm: "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==>
x \<otimes> y = y \<otimes> x"
shows "comm_group G"
- proof qed (simp_all add: m_comm)
+ by default (simp_all add: m_comm)
lemma comm_groupI:
fixes G (structure)
@@ -722,7 +722,7 @@
theorem (in group) subgroups_partial_order:
"partial_order (| carrier = {H. subgroup H G}, eq = op =, le = op \<subseteq> |)"
- proof qed simp_all
+ by default simp_all
lemma (in group) subgroup_self:
"subgroup (carrier G) G"