# HG changeset patch
# User haftmann
# Date 1384430589 -3600
# Node ID be1bc181bcde93b6c75cb6416dac322dc7520c11
# Parent  6ccc6130140ccbb8bd71b5e77c5db17d785ff606
explicit inclusion of data refinement theory into HOL-Library session

diff -r 6ccc6130140c -r be1bc181bcde src/HOL/ROOT
--- a/src/HOL/ROOT	Thu Nov 14 10:59:22 2013 +0100
+++ b/src/HOL/ROOT	Thu Nov 14 13:03:09 2013 +0100
@@ -43,6 +43,7 @@
     Code_Real_Approx_By_Float
     Code_Target_Numeral
     DAList
+    DAList_Multiset
     RBT_Mapping
     RBT_Set
     (*legacy tools*)