--- 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*)