src/HOL/BNF_Least_Fixpoint.thy
Sun, 09 Aug 2020 13:18:40 +0100 paulson elimination of some needless assumptions
Mon, 04 May 2020 17:35:29 +0200 Manuel Eberl New HOL simproc 'datatype_no_proper_subterm'
Thu, 14 Mar 2019 16:55:06 +0100 wenzelm more specific keyword kinds;
Sun, 06 Jan 2019 15:04:34 +0100 wenzelm isabelle update -u path_cartouches;
Sun, 26 Nov 2017 21:08:32 +0100 wenzelm more symbols;
Thu, 20 Jul 2017 16:28:43 +0100 blanchet strengthened tactic
Fri, 29 Jul 2016 09:49:23 +0200 Andreas Lochbihler add lemmas contributed by Peter Gammie
Thu, 07 Apr 2016 17:56:26 +0200 traytel removed duplicate lemma
Thu, 07 Apr 2016 17:56:22 +0200 traytel derive (co)rec uniformly from (un)fold
Sat, 18 Jul 2015 22:58:50 +0200 wenzelm isabelle update_cartouches;
Fri, 07 Nov 2014 11:28:37 +0100 traytel more complete fp_sugars for sum and prod;
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section;
Thu, 25 Sep 2014 16:35:56 +0200 desharna generate 'corec_transfer' for codatatypes
Thu, 25 Sep 2014 16:35:53 +0200 desharna generate 'rec_transfer' for datatypes
Thu, 25 Sep 2014 16:35:51 +0200 desharna generate 'dtor_corec_transfer' for codatatypes
Thu, 25 Sep 2014 16:35:50 +0200 desharna generate 'ctor_rec_transfer' for datatypes
Thu, 18 Sep 2014 16:47:40 +0200 blanchet moved old 'size' generator together with 'old_datatype'
Thu, 18 Sep 2014 16:47:40 +0200 blanchet moved datatype realizer to 'old_datatype' and colleagues
Tue, 16 Sep 2014 19:23:37 +0200 blanchet register 'prod' and 'sum' as datatypes, to allow N2M through them
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