2013-04-30 blanchet 2013-04-30 renamed "bnf_def" keyword to "bnf" (since it's not a definition, but rather a registration)
2013-04-25 traytel 2013-04-25 removed unnecessary assumptions in some theorems about cardinal exponentiation
2013-04-24 blanchet 2013-04-24 renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
2013-03-27 haftmann 2013-03-27 centralized various multiset operations in theory multiset; more conversions between multisets and lists respectively
2013-03-23 haftmann 2013-03-23 fundamental revision of big operators on sets
2013-03-18 traytel 2013-03-18 hide internal constants; tuned proofs
2013-03-13 traytel 2013-03-13 BNF uses fset defined via Lifting/Transfer rather than Quotient
2013-03-08 traytel 2013-03-08 some simp rules for fset
2012-11-21 hoelzl 2012-11-21 renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
2012-11-08 bulwahn 2012-11-08 adjusting proofs as the set_comprehension_pointfree simproc breaks some existing proofs
2012-10-16 popescua 2012-10-16 a few notations changed in HOL/BNF/Examples/Derivation_Trees
2012-10-16 popescua 2012-10-16 ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
2012-09-21 blanchet 2012-09-21 tuned whitespace
2012-09-21 blanchet 2012-09-21 renamed "Codatatype" directory "BNF" (and corresponding session) -- this opens the door to no-nonsense session names like "HOL-BNF-LFP"