src/HOL/BNF_Def.thy
Sun, 06 Jan 2019 15:04:34 +0100 wenzelm isabelle update -u path_cartouches;
Thu, 15 Feb 2018 12:11:00 +0100 wenzelm more symbols;
Wed, 10 Jan 2018 15:25:09 +0100 nipkow ran isabelle update_op on all sources
Sun, 26 Nov 2017 21:08:32 +0100 wenzelm more symbols;
Tue, 27 Jun 2017 00:07:34 +0200 blanchet more error checking
Sun, 11 Sep 2016 00:14:44 +0200 wenzelm tuned proofs;
Thu, 18 Aug 2016 11:10:07 +0200 traytel derive pred_mono property for BNFs
Fri, 13 May 2016 20:24:10 +0200 wenzelm eliminated use of empty "assms";
Wed, 17 Feb 2016 15:18:06 +0100 traytel derive transfer rule for predicator
Tue, 16 Feb 2016 22:28:19 +0100 traytel make predicator a first-class bnf citizen
Sun, 15 Nov 2015 12:39:51 +0100 wenzelm option "inductive_defs" controls exposure of def and mono facts;
Tue, 13 Oct 2015 09:21:15 +0200 haftmann prod_case as canonical name for product type eliminator
Tue, 13 Oct 2015 09:21:14 +0200 haftmann emphasized general nature of parameter
Tue, 13 Oct 2015 09:21:14 +0200 haftmann moved lemmas
Thu, 24 Sep 2015 12:21:19 +0200 traytel more useful properties of the relators
Thu, 27 Aug 2015 21:19:48 +0200 haftmann standardized some occurences of ancient "split" alias
Sat, 18 Jul 2015 22:58:50 +0200 wenzelm isabelle update_cartouches;
Mon, 16 Mar 2015 23:05:56 +0100 traytel BNF relators preserve reflexivity
Wed, 11 Feb 2015 13:50:11 +0100 Andreas Lochbihler add monotonicity lemmas for rel_fun
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:53 +0200 desharna generate 'rec_transfer' for datatypes
Tue, 16 Sep 2014 19:23:37 +0200 blanchet register 'prod' and 'sum' as datatypes, to allow N2M through them
Mon, 01 Sep 2014 13:53:34 +0200 desharna generate 'set_transfer' for BNFs
Mon, 01 Sep 2014 13:23:39 +0200 desharna generate 'rel_transfer' for BNFs
Wed, 06 Aug 2014 16:00:11 +0200 traytel handle deep nesting in N2M
Tue, 29 Jul 2014 23:39:35 +0200 blanchet header tuning
Thu, 24 Jul 2014 11:54:15 +0200 wenzelm more robust notation BNF_Def.convol, which is private to main HOL, but may cause syntax ambiguities nonetheless (e.g. List.thy);
Fri, 27 Jun 2014 10:11:44 +0200 blanchet merged two small theory files
Wed, 23 Apr 2014 10:23:26 +0200 blanchet added 'inj_map' as auxiliary BNF theorem
Thu, 06 Mar 2014 15:40:33 +0100 blanchet renamed 'fun_rel' to 'rel_fun'
Fri, 28 Feb 2014 17:54:52 +0100 traytel load Metis a little later
Tue, 25 Feb 2014 18:14:26 +0100 traytel joint work with blanchet: intermediate typedef for the input to fp-operations
Fri, 21 Feb 2014 00:09:56 +0100 blanchet adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
Wed, 12 Feb 2014 08:35:57 +0100 blanchet renamed '{prod,sum,bool,unit}_case' to 'case_...'
Wed, 29 Jan 2014 16:35:05 +0100 traytel made tactic more robust
Mon, 20 Jan 2014 21:32:41 +0100 blanchet moved 'fundef_cong' attribute (and other basic 'fun' stuff) up the dependency chain
Mon, 20 Jan 2014 18:24:56 +0100 blanchet tuning
Mon, 20 Jan 2014 18:24:56 +0100 blanchet made BNF compile after move to HOL
Mon, 20 Jan 2014 18:24:56 +0100 blanchet tuned comments
Mon, 20 Jan 2014 18:24:56 +0100 blanchet moved BNF files to 'HOL'
less more (0) tip