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 1927 6c5e3ac737d9
parent 1913 39951d71bfce
child 1935 266abc3ee228 
--- a/Nominal/FSet.thy	Wed Apr 21 13:39:34 2010 +0200
+++ b/Nominal/FSet.thy	Wed Apr 21 19:10:55 2010 +0200
@@ -589,6 +589,8 @@
   apply (simp_all)
   apply (case_tac "memb a A")
   apply (auto simp add: memb_def)[2]
+  apply (case_tac "list_eq2 (a # A) A")
+  apply (metis list_eq2.intros(3) list_eq2.intros(6))
   apply (metis list_eq2.intros(3) list_eq2.intros(4) list_eq2.intros(5) list_eq2.intros(6))
   apply (metis list_eq2.intros(1) list_eq2.intros(5) list_eq2.intros(6))
   apply (auto simp add: list_eq2_refl not_memb_delete_raw_ident)
nominal2