# HG changeset patch # User wenzelm # Date 1349875630 -7200 # Node ID b286e8f4756000aade7588fdd641391fc33f9f81 # Parent acafcac41690e0ff15a149d3cf4f825727b9671d avoid duplicate facts; diff -r acafcac41690 -r b286e8f47560 src/ZF/ex/Group.thy --- a/src/ZF/ex/Group.thy Wed Oct 10 15:21:26 2012 +0200 +++ b/src/ZF/ex/Group.thy Wed Oct 10 15:27:10 2012 +0200 @@ -203,11 +203,11 @@ qed lemma (in group) inv_comm: - assumes inv: "x \ y = \" + assumes "x \ y = \" and G: "x \ carrier(G)" "y \ carrier(G)" shows "y \ x = \" proof - - from G have "x \ y \ x = x \ \" by (auto simp add: inv) + from G have "x \ y \ x = x \ \" by (auto simp add: assms) with G show ?thesis by (simp del: r_one add: m_assoc) qed @@ -490,11 +490,12 @@ lemma (in group) subgroupI: assumes subset: "H \ carrier(G)" and non_empty: "H \ 0" - and inv: "!!a. a \ H ==> inv a \ H" - and mult: "!!a b. [|a \ H; b \ H|] ==> a \ b \ H" + and "!!a. a \ H ==> inv a \ H" + and "!!a b. [|a \ H; b \ H|] ==> a \ b \ H" shows "subgroup(H,G)" proof (simp add: subgroup_def assms) - show "\ \ H" by (rule one_in_subset) (auto simp only: assms) + show "\ \ H" + by (rule one_in_subset) (auto simp only: assms) qed @@ -595,7 +596,7 @@ "set_inv\<^bsub>G\<^esub> H == \h\H. {inv\<^bsub>G\<^esub> h}" -locale normal = subgroup + group + +locale normal = subgroup: subgroup + group + assumes coset_eq: "(\x \ carrier(G). H #> x = x <# H)" notation