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