diff --git a/Batteries/Data/DList.lean b/Batteries/Data/DList.lean
index 6a5450f0ba..00a2d9fadf 100644
--- a/Batteries/Data/DList.lean
+++ b/Batteries/Data/DList.lean
@@ -1,70 +1,2 @@
-/-
-Copyright (c) 2018 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-namespace Batteries
-/--
-A difference List is a Function that, given a List, returns the original
-contents of the difference List prepended to the given List.
-This structure supports `O(1)` `append` and `concat` operations on lists, making it
-useful for append-heavy uses such as logging and pretty printing.
--/
-structure DList (α : Type u) where
-  /-- "Run" a `DList` by appending it on the right by a `List α` to get another `List α`. -/
-  apply     : List α → List α
-  /-- The `apply` function of a `DList` is completely determined by the list `apply []`. -/
-  invariant : ∀ l, apply l = apply [] ++ l
-
-namespace DList
-variable {α : Type u}
-open List
-
-/-- `O(1)` (`apply` is `O(|l|)`). Convert a `List α` into a `DList α`. -/
-def ofList (l : List α) : DList α :=
-  ⟨(l ++ ·), fun t => by simp⟩
-
-/-- `O(1)` (`apply` is `O(1)`). Return an empty `DList α`. -/
-def empty : DList α :=
-  ⟨id, fun _ => rfl⟩
-
-instance : EmptyCollection (DList α) := ⟨DList.empty⟩
-
-/-- `O(apply())`. Convert a `DList α` into a `List α` by running the `apply` function. -/
-def toList : DList α → List α
-  | ⟨f, _⟩ => f []
-
-/-- `O(1)` (`apply` is `O(1)`). A `DList α` corresponding to the list `[a]`. -/
-def singleton (a : α) : DList α where
-  apply     := fun t => a :: t
-  invariant := fun _ => rfl
-
-/-- `O(1)` (`apply` is `O(1)`). Prepend `a` on a `DList α`. -/
-def cons : α → DList α → DList α
-  | a, ⟨f, h⟩ => {
-    apply     := fun t => a :: f t
-    invariant := by intro t; simp; rw [h]
-  }
-
-/-- `O(1)` (`apply` is `O(1)`). Append two `DList α`. -/
-def append : DList α → DList α → DList α
-  | ⟨f, h₁⟩, ⟨g, h₂⟩ => {
-    apply     := f ∘ g
-    invariant := by
-      intro t
-      show f (g t) = (f (g [])) ++ t
-      rw [h₁ (g t), h₂ t, ← append_assoc (f []) (g []) t, ← h₁ (g [])]
-    }
-
-/-- `O(1)` (`apply` is `O(1)`). Append an element at the end of a `DList α`. -/
-def push : DList α → α → DList α
-  | ⟨f, h⟩, a => {
-    apply     := fun t => f (a :: t)
-    invariant := by
-      intro t
-      show f (a :: t) = f (a :: nil) ++ t
-      rw [h [a], h (a::t), append_assoc (f []) [a] t]
-      rfl
-  }
-
-instance : Append (DList α) := ⟨DList.append⟩
+import Batteries.Data.DList.Basic
+import Batteries.Data.DList.Lemmas
diff --git a/Batteries/Data/DList/Basic.lean b/Batteries/Data/DList/Basic.lean
new file mode 100644
index 0000000000..51228eb4b4
--- /dev/null
+++ b/Batteries/Data/DList/Basic.lean
@@ -0,0 +1,80 @@
+/-
+Copyright (c) 2018 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+namespace Batteries
+/--
+A difference List is a Function that, given a List, returns the original
+contents of the difference List prepended to the given List.
+This structure supports `O(1)` `append` and `push` operations on lists, making it
+useful for append-heavy uses such as logging and pretty printing.
+-/
+structure DList (α : Type u) where
+  /-- "Run" a `DList` by appending it on the right by a `List α` to get another `List α`. -/
+  apply     : List α → List α
+  /-- The `apply` function of a `DList` is completely determined by the list `apply []`. -/
+  invariant : ∀ l, apply l = apply [] ++ l
+
+namespace DList
+variable {α : Type u}
+open List
+
+/-- `O(1)` (`apply` is `O(|l|)`). Convert a `List α` into a `DList α`. -/
+def ofList (l : List α) : DList α :=
+  ⟨(l ++ ·), fun t => by simp⟩
+
+/-- `O(1)` (`apply` is `O(1)`). Return an empty `DList α`. -/
+def empty : DList α :=
+  ⟨id, fun _ => rfl⟩
+
+instance : EmptyCollection (DList α) := ⟨DList.empty⟩
+
+/-- `O(apply())`. Convert a `DList α` into a `List α` by running the `apply` function. -/
+def toList : DList α → List α
+  | ⟨f, _⟩ => f []
+
+/-- `O(1)` (`apply` is `O(1)`). A `DList α` corresponding to the list `[a]`. -/
+def singleton (a : α) : DList α where
+  apply     := fun t => a :: t
+  invariant := fun _ => rfl
+
+/-- `O(1)` (`apply` is `O(1)`). Prepend `a` on a `DList α`. -/
+def cons : α → DList α → DList α
+  | a, ⟨f, h⟩ => {
+    apply     := fun t => a :: f t
+    invariant := by intro t; simp; rw [h]
+  }
+
+/-- `O(1)` (`apply` is `O(1)`). Append two `DList α`. -/
+def append : DList α → DList α → DList α
+  | ⟨f, h₁⟩, ⟨g, h₂⟩ => {
+    apply     := f ∘ g
+    invariant := by
+      intro t
+      show f (g t) = (f (g [])) ++ t
+      rw [h₁ (g t), h₂ t, ← append_assoc (f []) (g []) t, ← h₁ (g [])]
+    }
+
+/-- `O(1)` (`apply` is `O(1)`). Append an element at the end of a `DList α`. -/
+def push : DList α → α → DList α
+  | ⟨f, h⟩, a => {
+    apply     := fun t => f (a :: t)
+    invariant := by
+      intro t
+      show f (a :: t) = f (a :: nil) ++ t
+      rw [h [a], h (a::t), append_assoc (f []) [a] t]
+      rfl
+  }
+
+instance : Append (DList α) := ⟨DList.append⟩
+
+/-- Convert a lazily-evaluated `List` to a `DList` -/
+def lazy_ofList (l : Thunk (List α)) : DList α :=
+  ⟨fun xs => l.get ++ xs, fun t => by simp⟩
+
+/-- Concatenates a list of difference lists to form a single difference list. Similar to
+`List.join`. -/
+def join {α : Type _} : List (DList α) → DList α
+  | [] => DList.empty
+  | x :: xs => x ++ DList.join xs
diff --git a/Batteries/Data/DList/Lemmas.lean b/Batteries/Data/DList/Lemmas.lean
new file mode 100644
index 0000000000..61f8885864
--- /dev/null
+++ b/Batteries/Data/DList/Lemmas.lean
@@ -0,0 +1,63 @@
+/-
+Copyright (c) 2017 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Batteries.Data.DList.Basic
+
+/-!
+# Difference list
+
+This file provides a few results about `DList`.
+
+A difference list is a function that, given a list, returns the original content of the
+difference list prepended to the given list. It is useful to represent elements of a given type
+as `a₁ + ... + aₙ` where `+ : α → α → α` is any operation, without actually computing.
+
+This structure supports `O(1)` `append` and `push` operations on lists, making it
+useful for append-heavy uses such as logging and pretty printing.
+-/
+
+universe u
+
+namespace Batteries.DList
+
+open Function
+
+variable {α : Type u}
+
+attribute [local simp] Function.comp
+
+attribute [local simp] ofList toList empty singleton cons push append
+
+theorem toList_ofList (l : List α) : DList.toList (DList.ofList l) = l := by
+  cases l; rfl; simp only [DList.toList, DList.ofList, List.cons_append, List.append_nil]
+
+theorem ofList_toList (l : DList α) : DList.ofList (DList.toList l) = l := by
+   obtain ⟨app, inv⟩ := l
+   simp only [ofList, toList, mk.injEq]
+   funext x
+   rw [(inv x)]
+
+theorem toList_empty : toList (@empty α) = [] := by simp
+
+theorem toList_singleton (x : α) : toList (singleton x) = [x] := by simp
+
+theorem toList_append (l₁ l₂ : DList α) : toList (l₁ ++ l₂) = toList l₁ ++ toList l₂ := by
+  obtain ⟨_, l₁_invariant⟩ := l₁; cases l₂; simp; rw [l₁_invariant]
+
+theorem toList_cons (x : α) (l : DList α) : toList (cons x l) = x :: toList l := by
+  cases l; simp
+
+theorem toList_push (x : α) (l : DList α) : toList (push l x) = toList l ++ [x] := by
+  obtain ⟨_, l_invariant⟩ := l; simp; rw [l_invariant]
+
+@[simp]
+theorem DList_singleton {α : Type _} {a : α} : singleton a = lazy_ofList [a] :=
+  rfl
+
+@[simp]
+theorem DList_lazy {α : Type _} {l : List α} : lazy_ofList l = ofList l :=
+  rfl
+
+end Batteries.DList
diff --git a/Batteries/StdDeprecations.lean b/Batteries/StdDeprecations.lean
index cb49a3bdbf..74a00f4f5a 100644
--- a/Batteries/StdDeprecations.lean
+++ b/Batteries/StdDeprecations.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
 import Batteries.Tactic.Alias
-import Batteries.Data.DList
+import Batteries.Data.DList.Basic
 import Batteries.Data.PairingHeap
 import Batteries.Data.BinomialHeap.Basic
 import Batteries.Data.HashMap.Basic