src/HOL/Library/Dlist.thy
changeset 46133 d9fe85d3d2cd
parent 45990 b7b905b23b2a
child 46565 ad21900e0ee9
     1.1 --- a/src/HOL/Library/Dlist.thy	Fri Jan 06 10:19:49 2012 +0100
     1.2 +++ b/src/HOL/Library/Dlist.thy	Fri Jan 06 10:19:49 2012 +0100
     1.3 @@ -74,7 +74,7 @@
     1.4    "length dxs = List.length (list_of_dlist dxs)"
     1.5  
     1.6  definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b \<Rightarrow> 'b" where
     1.7 -  "fold f dxs = More_List.fold f (list_of_dlist dxs)"
     1.8 +  "fold f dxs = List.fold f (list_of_dlist dxs)"
     1.9  
    1.10  definition foldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b \<Rightarrow> 'b" where
    1.11    "foldr f dxs = List.foldr f (list_of_dlist dxs)"