# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1271227014 -7200
# Node ID 1d6a0aeef4a1a2ea1bfa5b6fad80760287c49848
# Parent  2ccc1b00377c187620cf0cad9ee8ae37aed5782b
merge part: delete_rsp

diff -r 2ccc1b00377c -r 1d6a0aeef4a1 Nominal/FSet.thy
--- a/Nominal/FSet.thy	Wed Apr 14 08:35:31 2010 +0200
+++ b/Nominal/FSet.thy	Wed Apr 14 08:36:54 2010 +0200
@@ -278,6 +278,10 @@
   "memb x (delete_raw xs y) = (memb x xs \<and> x \<noteq> y)"
   by (induct xs arbitrary: x y) (auto simp add: memb_def)
 
+lemma delete_raw_rsp:
+  "l \<approx> r \<Longrightarrow> delete_raw l x \<approx> delete_raw r x"
+  by (simp add: memb_def[symmetric] memb_delete_raw)
+
 lemma [quot_respect]:
   "(op \<approx> ===> op = ===> op \<approx>) delete_raw delete_raw"
   by (simp add: memb_def[symmetric] memb_delete_raw)