src/HOL/BNF/Basic_BNFs.thy
2013-10-22 traytel 2013-10-22 removed junk
2013-10-22 traytel 2013-10-22 define a trivial nonemptiness witness if none is provided
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-07-15 traytel 2013-07-15 killed unused theorems
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-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-03-18 traytel 2013-03-18 hide internal constants; tuned proofs
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"