# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1271227358 -7200
# Node ID faa7e6033f2e5fef09df5a9b5d511f0eadf4b900
# Parent  1d6a0aeef4a1a2ea1bfa5b6fad80760287c49848
merge

diff -r 1d6a0aeef4a1 -r faa7e6033f2e Nominal/FSet.thy
--- a/Nominal/FSet.thy	Wed Apr 14 08:36:54 2010 +0200
+++ b/Nominal/FSet.thy	Wed Apr 14 08:42:38 2010 +0200
@@ -483,8 +483,6 @@
   "fset_to_set (finsert (h :: 'a) t) = insert h (fset_to_set t)"
   by (lifting set.simps)
 
-thm memb_def[symmetric, THEN meta_eq_to_obj_eq]
-
 lemma in_fset_to_set:
   "x \<in> fset_to_set S \<equiv> x |\<in>| S"
   by (lifting memb_def[symmetric])