src/HOL/BNF/BNF_Def.thy
2013-09-12 traytel 2013-09-12 simplified derivation of in_rel
2013-09-12 traytel 2013-09-12 removed unused/inlinable theorems
2013-08-12 traytel 2013-08-12 eliminated bogus assumption from theorem (that was instantiated with refl and resulted in flexflex pairs)
2013-07-28 traytel 2013-07-28 more converse(p) theorems; tuned proofs;
2013-07-25 traytel 2013-07-25 transfer rule for {c,d}tor_{,un}fold
2013-07-25 traytel 2013-07-25 two useful relation theorems
2013-07-22 traytel 2013-07-22 transfer rule for map (not yet registered as a transfer rule)
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-05-08 traytel 2013-05-08 store proper theorems even for fixed points that have no passive live variables
2013-05-08 traytel 2013-05-08 stronger monotonicity property for relators
2013-05-07 traytel 2013-05-07 removed dead internal constants/theorems
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)
2012-09-23 blanchet 2012-09-23 generate "rel_as_srel" and "rel_flip" properties
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"