changeset 35688 | cfe0accda6e3 |
parent 35303 | 816e48d60b13 |
child 36112 | 7fa17a225852 |
--- a/src/HOL/Library/Dlist.thy Wed Mar 10 15:29:21 2010 +0100 +++ b/src/HOL/Library/Dlist.thy Wed Mar 10 15:29:22 2010 +0100 @@ -123,8 +123,6 @@ "list_of_dlist (filter P dxs) = List.filter P (list_of_dlist dxs)" by (simp add: filter_def) -declare null_def [code] member_def [code] length_def [code] fold_def [code] -- {* explicit is better than implicit *} - section {* Implementation of sets by distinct lists -- canonical! *}