src/HOL/Basic_BNFs.thy
16 months ago wenzelm 2017-11-26 more symbols;
2016-02-17 blanchet 2016-02-17 making 'pred_inject' a first-class BNF citizen
2016-02-16 traytel 2016-02-16 make predicator a first-class bnf citizen
2015-11-15 wenzelm 2015-11-15 option "inductive_defs" controls exposure of def and mono facts;
2015-08-27 haftmann 2015-08-27 standardized some occurences of ancient "split" alias
2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2014-11-07 traytel 2014-11-07 more complete fp_sugars for sum and prod; tuned; removed theorem duplicates; removed obsolete Lifting_{Option,Product,Sum} theories
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-09-25 desharna 2014-09-25 generate 'rec_transfer' for datatypes
2014-03-13 haftmann 2014-03-13 tuned proofs
2014-03-06 blanchet 2014-03-06 renamed 'fun_rel' to 'rel_fun'
2014-03-06 blanchet 2014-03-06 renamed 'prod_rel' to 'rel_prod'
2014-03-06 blanchet 2014-03-06 renamed 'sum_rel' to 'rel_sum'
2014-03-06 traytel 2014-03-06 move special BNFs used for composition only to BNF_Comp; use local copy of identity function that gets unfolded later for ID
2014-03-06 blanchet 2014-03-06 renamed 'map_pair' to 'map_prod'
2014-03-06 blanchet 2014-03-06 renamed 'map_sum' to 'sum_map'
2014-02-28 traytel 2014-02-28 load Metis a little later
2014-02-24 traytel 2014-02-24 clarified interaction with dead variables in the composition of BNFs
2014-01-20 blanchet 2014-01-20 rationalized lemmas
2014-01-20 blanchet 2014-01-20 move BNF_LFP up the dependency chain
2014-01-20 blanchet 2014-01-20 dissolved BNF session
2014-01-20 blanchet 2014-01-20 made BNF compile after move to HOL
2014-01-20 blanchet 2014-01-20 moved BNF files to 'HOL'