src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML
2013-09-20 blanchet 2013-09-20 have "datatype_new_compat" register induction and recursion theorems in nested case
2013-09-17 blanchet 2013-09-17 return right theorems
2013-09-13 blanchet 2013-09-13 don't wrongly destroy sum types in coiterators
2013-09-09 blanchet 2013-09-09 include map theorems in datastructure for "primcorec"
2013-09-09 blanchet 2013-09-09 enriched data structure with necessary theorems
2013-08-30 blanchet 2013-08-30 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository