src/HOL/BNF/Tools/bnf_lfp.ML
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-28 blanchet 2012-09-28 renamed ML file in preparation for next step
2012-09-28 blanchet 2012-09-28 killed temporary "data_raw" and "codata_raw" now that the examples have been ported to "data" and "codata"
2012-09-26 blanchet 2012-09-26 tweaked theorem names (in particular, dropped s's)
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-26 blanchet 2012-09-26 use singular since there is always only one theorem
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"