src/HOL/BNF/Tools/bnf_gfp.ML
2012-09-26 blanchet 2012-09-26 generate high-level "maps", "sets", and "rels" properties
2012-09-26 blanchet 2012-09-26 use singular since there is always only one theorem
2012-09-26 blanchet 2012-09-26 renamed "dtor_rel_coinduct" etc. to "dtor_coinduct"
2012-09-26 blanchet 2012-09-26 renamed "dtor_coinduct" etc. to "dtor_map_coinduct"
2012-09-26 blanchet 2012-09-26 leave out some internal theorems unless "bnf_note_all" is set
2012-09-23 blanchet 2012-09-23 renamed coinduction principles to have "dtor" in the name
2012-09-23 blanchet 2012-09-23 renamed "set_incl" etc. to have "ctor" or "dtor" in the name
2012-09-23 blanchet 2012-09-23 renamed low-level "map_unique" to have "ctor" or "dtor" in the name
2012-09-23 blanchet 2012-09-23 renamed low-level "set_simps" and "set_induct" to have "ctor" or "dtor" in the name
2012-09-23 blanchet 2012-09-23 renamed "map_simps" to "{c,d}tor_maps"
2012-09-23 blanchet 2012-09-23 simplified fact policies
2012-09-23 blanchet 2012-09-23 started work on generation of "rel" theorems
2012-09-21 blanchet 2012-09-21 renamed LFP low-level rel property to have ctor not dtor in its name
2012-09-21 blanchet 2012-09-21 renamed "rel_simp" to "dtor_rel" and similarly for "srel"
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"