src/HOL/BNF/Tools/bnf_util.ML
2013-05-31 blanchet 2013-05-31 tuning
2013-05-31 blanchet 2013-05-31 renamed util function
2013-05-20 wenzelm 2013-05-20 tuned signature;
2013-05-07 blanchet 2013-05-07 move function to library
2013-05-07 traytel 2013-05-07 tuned
2013-05-07 traytel 2013-05-07 got rid of the set based relator---use (binary) predicate based relator instead
2013-05-02 blanchet 2013-05-02 one more lib function
2013-04-26 blanchet 2013-04-26 more intuitive syntax for equality-style discriminators of nullary constructors
2013-04-26 blanchet 2013-04-26 changed discriminator default: avoid mixing ctor and dtor views
2013-04-24 blanchet 2013-04-24 honor user-specified name for relator + generalize syntax
2013-04-24 blanchet 2013-04-24 derive "map_cong"
2013-04-24 blanchet 2013-04-24 killed dead code
2013-04-24 blanchet 2013-04-24 honor user-specified name for map function
2013-04-24 blanchet 2013-04-24 honor user-specified set function names
2012-10-12 wenzelm 2012-10-12 discontinued typedef with alternative name;
2012-10-12 wenzelm 2012-10-12 discontinued typedef with implicit set_def;
2012-09-30 blanchet 2012-09-30 tuning
2012-09-27 blanchet 2012-09-27 avoid another brand of trivial "disc_rel" theorems (which made the simplifier loop for all single-constructor types)
2012-09-26 blanchet 2012-09-26 generate high-level "maps", "sets", and "rels" properties
2012-09-23 blanchet 2012-09-23 started work on generation of "rel" theorems
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"