author | Cezary Kaliszyk <kaliszyk@in.tum.de> |
Fri, 26 Aug 2011 09:31:56 +0900 | |
changeset 44512 | 5e0f9e0e32fb |
parent 44498 | a4cbf5668a54 |
child 44513 | f7259c9064ea |
--- 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"