src/HOL/BNF/Tools/bnf_lfp_compat.ML
Tue, 24 Sep 2013 00:01:10 +0200 blanchet register codatatypes with Nitpick
Fri, 20 Sep 2013 12:04:48 +0200 blanchet took out spurious attributes (no need for several code equations / simps for thesame constants)
Fri, 20 Sep 2013 11:44:30 +0200 blanchet have "datatype_new_compat" register induction and recursion theorems in nested case
Fri, 30 Aug 2013 12:12:41 +0200 blanchet renamed command to clarify connection with BNF
Fri, 30 Aug 2013 11:27:23 +0200 blanchet moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
less more (0) tip