src/HOL/Tools/BNF/bnf_def.ML
2014-08-18 desharna 2014-08-18 generate 'map_cong_simp' for BNFs
2014-08-18 desharna 2014-08-18 generate 'inj_map_strong' for BNFs
2014-08-18 desharna 2014-08-18 note 'inj_map' more often
2014-08-18 desharna 2014-08-18 generate property 'rel_mono_strong' for BNFs
2014-08-18 desharna 2014-08-18 renamed 'rel_mono_strong' to 'rel_mono_strong0'
2014-08-14 desharna 2014-08-14 generate 'rel_map' theorem for BNFs
2014-07-25 blanchet 2014-07-25 tuning
2014-07-24 blanchet 2014-07-24 use the noted theorems in 'BNF_Comp'
2014-07-24 blanchet 2014-07-24 use the noted theorem whenever possible, also in 'BNF_Def'
2014-07-17 desharna 2014-07-17 add mk_Trueprop_mem utility function
2014-07-09 blanchet 2014-07-09 got rid of a pointer equality
2014-06-27 blanchet 2014-06-27 compile
2014-06-24 desharna 2014-06-24 tune the implementation of 'rel_coinduct'
2014-06-24 desharna 2014-06-24 generate 'rel_coinduct0' theorem for codatatypes
2014-05-08 desharna 2014-05-08 note map_id0 more often
2014-05-08 desharna 2014-05-08 generate 'map_ident' theorem for BNFs
2014-04-28 blanchet 2014-04-28 more reliable 'name_of_bnf'
2014-04-23 blanchet 2014-04-23 made SML/NJ happier
2014-04-23 blanchet 2014-04-23 localize new size function generation code
2014-04-23 blanchet 2014-04-23 added 'inj_map' as auxiliary BNF theorem
2014-04-10 kuncar 2014-04-10 revert idiomatic handling of namings from 5a93b8f928a2 because in combination with Named_Target.theory_init global names are sometimes created
2014-04-10 kuncar 2014-04-10 don't forget to init Interpretation and transfer theorems in the interpretation hook
2014-04-03 blanchet 2014-04-03 added same idiomatic handling of namings for Ctr_Sugar/BNF-related interpretation hooks as for typedef and (old-style) datatypes
2014-04-01 blanchet 2014-04-01 added BNF interpretation hook
2014-03-10 traytel 2014-03-10 unfold intermediate definitions after sealing the bnf
2014-03-06 blanchet 2014-03-06 renamed 'fun_rel' to 'rel_fun'
2014-03-03 blanchet 2014-03-03 make 'typedef' optional, depending on size of original type
2014-02-14 blanchet 2014-02-14 allow different functions to recurse on the same type, like in the old package
2014-02-12 blanchet 2014-02-12 iteration n in the 'default' vs. 'update_new' vs. 'update' saga -- 'update' makes sense now that we honor the canonical order on 'merge' (as opposed to raising 'DUP')
2014-02-12 blanchet 2014-02-12 more liberal merging of BNFs and constructor sugar * * * make sure that the cache doesn't produce 'DUP's
2014-02-07 blanchet 2014-02-07 reverted a87e49f4336d -- overwriting of data entries yields to merge problems later
2014-02-06 blanchet 2014-02-06 allow multiple registration of the same type, the last wins
2014-01-31 traytel 2014-01-31 less hermetic tactics
2014-01-20 blanchet 2014-01-20 adjusted comments
2014-01-20 blanchet 2014-01-20 avoid nested 'Tools' directories