# HG changeset patch
# User haftmann
# Date 1342559487 -7200
# Node ID 8a1ef12f7e6da19f8178e473922da6b1f9d38f69
# Parent  39bfb2844b9ed3c616257696990615b1fa5ade64
explicitly import Dlist theory into library

diff -r 39bfb2844b9e -r 8a1ef12f7e6d src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Tue Jul 17 23:11:24 2012 +0200
+++ b/src/HOL/Library/Library.thy	Tue Jul 17 23:11:27 2012 +0200
@@ -12,6 +12,7 @@
   ContNotDenum
   Convex
   Countable
+  Dlist
   Eval_Witness
   Extended_Nat
   FinFun