src/HOL/BNF_Least_Fixpoint.thy
Thu, 11 Sep 2014 19:41:45 +0200 blanchet compile
Thu, 11 Sep 2014 19:32:36 +0200 blanchet updated news
Thu, 11 Sep 2014 18:54:36 +0200 blanchet renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
Tue, 09 Sep 2014 20:51:36 +0200 blanchet removed debugging junk
Tue, 09 Sep 2014 20:51:36 +0200 blanchet renamed ML file and module
Tue, 09 Sep 2014 20:51:36 +0200 blanchet made datatype realizer plugin work for new-style datatypes with no nesting
Mon, 08 Sep 2014 14:03:01 +0200 blanchet extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
Thu, 04 Sep 2014 11:20:59 +0200 blanchet tweaked setup for datatype realizer
Thu, 04 Sep 2014 09:02:43 +0200 blanchet tuned size function generation
Wed, 03 Sep 2014 00:31:37 +0200 blanchet tuning
Wed, 03 Sep 2014 00:06:19 +0200 blanchet more compatibility functions
Tue, 02 Sep 2014 12:09:13 +0200 blanchet tuning
Mon, 01 Sep 2014 16:34:40 +0200 blanchet renamed BNF theories
less more (0) tip