Mercurial Mercurial > hg > nominal2 / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
merge
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Wed, 14 Apr 2010 08:42:38 +0200
changeset 1826 faa7e6033f2e
parent 1825 1d6a0aeef4a1
child 1829 ac8cb569a17b
child 1837 edc2a52cd457
merge
Nominal/FSet.thy file | annotate | diff | comparison | revisions 
--- 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