src/HOL/BNF/BNF.thy
2014-01-16 blanchet 2014-01-16 hide short const name
2013-12-18 traytel 2013-12-18 express weak pullback property of bnfs only in terms of the relator
2013-11-27 traytel 2013-11-27 command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
2013-11-20 blanchet 2013-11-20 moved 'coinduction' proof method to 'HOL'
2013-11-20 blanchet 2013-11-20 move registration of countable set type as BNF to its own theory file (+ renamed theory)
2013-10-02 traytel 2013-10-02 new coinduction method
2013-08-21 traytel 2013-08-21 tuned theory imports
2013-07-25 traytel 2013-07-25 transfer rule for {c,d}tor_{,un}fold
2013-07-22 traytel 2013-07-22 transfer rule for map (not yet registered as a transfer rule)
2013-05-07 traytel 2013-05-07 removed dead internal constants/theorems
2013-05-07 traytel 2013-05-07 tuned
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"