src/HOL/Library/Library.thy

--- a/src/HOL/Library/Library.thy	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/Library/Library.thy	Mon Jan 20 18:24:56 2014 +0100
@@ -5,13 +5,14 @@
   BigO
   Binomial
   Bit
+  BNF_Decl
   Boolean_Algebra
   Char_ord
   Continuity
   ContNotDenum
   Convex
   Countable
-  Countable_Set
+  Countable_Set_Type
   Debug
   Diagonal_Subsequence
   Dlist
@@ -37,6 +38,7 @@
   Kleene_Algebra
   Mapping
   Monad_Syntax
+  More_BNFs
   Multiset
   Numeral_Type
   OptionalSugar