changeset 45694 | 4a8743618257 |
parent 43764 | 366d5726de09 |
child 45927 | e0305e4f02c9 |
--- a/src/HOL/Library/Dlist.thy Wed Nov 30 16:05:15 2011 +0100 +++ b/src/HOL/Library/Dlist.thy Wed Nov 30 16:27:10 2011 +0100 @@ -11,7 +11,7 @@ typedef (open) 'a dlist = "{xs::'a list. distinct xs}" morphisms list_of_dlist Abs_dlist proof - show "[] \<in> ?dlist" by simp + show "[] \<in> {xs. distinct xs}" by simp qed lemma dlist_eq_iff: