src/HOL/BNF/Tools/bnf_def.ML
2013-04-30 blanchet 2013-04-30 lowercase type constructor, for consistency (cf. fp_result not FP_result nor FP_Result)
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-29 blanchet 2013-04-29 create data structure for storing (co)datatype information
2013-04-27 wenzelm 2013-04-27 uniform Proof.context for hyp_subst_tac;
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 renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
2013-04-24 blanchet 2013-04-24 added "fundef_cong" attribute to "map_cong"
2013-04-24 blanchet 2013-04-24 derive "map_cong"
2013-04-24 blanchet 2013-04-24 renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
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
2013-03-27 wenzelm 2013-03-27 tuned signature and module arrangement;
2012-09-28 blanchet 2012-09-28 modernized example
2012-09-27 traytel 2012-09-27 tuned tactic; got rid of substs_tac alias
2012-09-26 blanchet 2012-09-26 got rid of other instance of shaky "Thm.generalize"
2012-09-26 blanchet 2012-09-26 tweaked theorem names (in particular, dropped s's)
2012-09-26 blanchet 2012-09-26 fixed "rels" + split them into injectivity and distinctness
2012-09-26 blanchet 2012-09-26 generate high-level "coinduct" and "strong_coinduct" properties
2012-09-26 blanchet 2012-09-26 generate high-level "maps", "sets", and "rels" properties
2012-09-23 blanchet 2012-09-23 simplified fact policies
2012-09-23 blanchet 2012-09-23 generate "rel_as_srel" and "rel_flip" properties
2012-09-23 blanchet 2012-09-23 started work on generation of "rel" theorems
2012-09-21 blanchet 2012-09-21 fixed a few names that escaped the renaming
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"