2013-09-03 wenzelm 2013-09-03 tuned proofs -- clarified flow of facts wrt. calculation;
2013-08-29 blanchet 2013-08-29 renamed BNF fact
2013-08-29 blanchet 2013-08-29 renamed BNF fact
2013-08-29 blanchet 2013-08-29 compile
2013-08-29 blanchet 2013-08-29 renamed BNF axiom
2013-08-21 traytel 2013-08-21 tuned theory imports
2013-08-13 traytel 2013-08-13 got rid of the dependency of Lifting_* on the function package; use the original rel constants for basic BNFs;
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)
2013-07-13 traytel 2013-07-13 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
2013-07-07 traytel 2013-07-07 Func -> Func_option, Ffunc -> Func (avoids dependence of codatatypes on the option type)
2013-07-05 traytel 2013-07-05 tuned spelling
2013-05-07 traytel 2013-05-07 got rid of the set based relator---use (binary) predicate based relator instead
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"