changeset 44512 | 5e0f9e0e32fb |
parent 44204 | 3cdc4176638c |
child 45129 | 1fce03e3e8ad |
--- a/src/HOL/Quotient_Examples/FSet.thy Thu Aug 25 19:09:39 2011 +0200 +++ b/src/HOL/Quotient_Examples/FSet.thy Fri Aug 26 09:31:56 2011 +0900 @@ -196,7 +196,11 @@ lemma member_rsp [quot_respect]: shows "(op \<approx> ===> op =) List.member List.member" - by (auto intro!: fun_relI simp add: mem_def) +proof + fix x y assume "x \<approx> y" + then show "List.member x = List.member y" + unfolding fun_eq_iff by simp +qed lemma nil_rsp [quot_respect]: shows "(op \<approx>) Nil Nil"