src/HOL/BNF/Tools/bnf_comp.ML
2013-05-17 wenzelm 2013-05-17 proper option quick_and_dirty;
2013-05-07 traytel 2013-05-07 do not unfold the definition of the relator as it is not defined in terms of srel anymore
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 lowercase type constructor, for consistency (cf. fp_result not FP_result nor FP_Result)
2013-04-25 traytel 2013-04-25 removed unnecessary assumptions in some theorems about cardinal exponentiation
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 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-11-13 traytel 2012-11-13 made SMLNJ happier
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-10-04 traytel 2012-10-04 made SML/NJ happier
2012-10-04 traytel 2012-10-04 do not expose details of internal data structures for composition of BNFs
2012-09-30 blanchet 2012-09-30 fixed quick-and-dirty mode
2012-09-28 traytel 2012-09-28 tuned tactics
2012-09-26 blanchet 2012-09-26 parameterized "subst_tac"
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-21 blanchet 2012-09-21 clean up lemmas used for composition
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"