src/HOL/Basic_BNFs.thy
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;
Wed, 17 Feb 2016 17:08:36 +0100 blanchet making 'pred_inject' a first-class BNF citizen
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;
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;
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
Thu, 13 Mar 2014 08:56:08 +0100 haftmann tuned proofs
Thu, 06 Mar 2014 15:40:33 +0100 blanchet renamed 'fun_rel' to 'rel_fun'
Thu, 06 Mar 2014 15:29:18 +0100 blanchet renamed 'prod_rel' to 'rel_prod'
Thu, 06 Mar 2014 15:25:21 +0100 blanchet renamed 'sum_rel' to 'rel_sum'
Thu, 06 Mar 2014 14:14:54 +0100 traytel move special BNFs used for composition only to BNF_Comp;
Thu, 06 Mar 2014 13:36:48 +0100 blanchet renamed 'map_pair' to 'map_prod'
Thu, 06 Mar 2014 13:36:15 +0100 blanchet renamed 'map_sum' to 'sum_map'
Fri, 28 Feb 2014 17:54:52 +0100 traytel load Metis a little later
Mon, 24 Feb 2014 10:16:10 +0100 traytel clarified interaction with dead variables in the composition of BNFs
Mon, 20 Jan 2014 20:42:43 +0100 blanchet rationalized lemmas
Mon, 20 Jan 2014 20:21:12 +0100 blanchet move BNF_LFP up the dependency chain
Mon, 20 Jan 2014 18:24:56 +0100 blanchet dissolved BNF session
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 moved BNF files to 'HOL'
less more (0) tip