Mercurial Mercurial > hg > nominal2 / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/FSet.thy
changeset 1826 faa7e6033f2e
parent 1825 1d6a0aeef4a1
child 1860 d3fe17786640 
--- 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])
nominal2