src/HOL/Library/Library.thy
changeset 48283 8a1ef12f7e6d
parent 48188 dcfe2c92fc7c
child 48427 571cb1df0768
--- 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