changeset 26203 | 9625f3579b48 |
parent 23463 | 9953ff53cc64 |
child 26310 | f8a7fac36e13 |
--- a/src/HOL/Algebra/Coset.thy Wed Mar 05 21:33:59 2008 +0100 +++ b/src/HOL/Algebra/Coset.thy Wed Mar 05 21:42:21 2008 +0100 @@ -826,7 +826,7 @@ includes group G shows "H \<in> rcosets H" proof - - from _ `subgroup H G` have "H #> \<one> = H" + from _ subgroup_axioms have "H #> \<one> = H" by (rule coset_join2) auto then show ?thesis by (auto simp add: RCOSETS_def)