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.
removed a sorry
authorChristian Urban <urbanc@in.tum.de>
Wed, 21 Apr 2010 10:08:47 +0200
changeset 1912 0a857f662e4c
parent 1911 60b5c61d3de2
child 1913 39951d71bfce
removed a sorry
Nominal/FSet.thy file | annotate | diff | comparison | revisions 
--- a/Nominal/FSet.thy	Tue Apr 20 18:24:50 2010 +0200
+++ b/Nominal/FSet.thy	Wed Apr 21 10:08:47 2010 +0200
@@ -603,7 +603,7 @@
   have "fcard_raw l = 0" by fact
   then have "\<forall>x. \<not> memb x l" using memb_card_not_0[of _ l] by auto
   then have z: "l = []" using no_memb_nil by auto
-  then have "r = []" sorry
+  then have "r = []" using `l \<approx> r` by simp
   then show ?case using z list_eq2_refl by simp
 next
   case (Suc m)
nominal2