2013-08-13 kuncar 2013-08-13 remove unnecessary dependencies on Library/Quotient_*
2013-07-16 traytel 2013-07-16 use transfer/lifting for proving countable set and multisets being BNFs
2013-07-15 traytel 2013-07-15 killed unused theorems
2013-07-15 traytel 2013-07-15 eliminate duplicated theorems (thanks to "Auto solve_direct" in jEdit)
2012-11-21 hoelzl 2012-11-21 renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set