src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
2014-08-10 wenzelm 2014-08-10 merged -- with manual conflict resolution for src/HOL/SMT_Examples/SMT_Examples.certs2, src/HOL/SMT_Examples/SMT_Word_Examples.certs2, src/Doc/Prog_Prove/document/intro-isabelle.tex;
2014-07-28 desharna 2014-07-28 made tactic more robust w.r.t. dead variables; tuned;
2014-08-07 blanchet 2014-08-07 generate nicer 'set' theorems for (co)datatypes
2014-07-30 desharna 2014-07-30 generate 'set_induct' theorem for codatatypes
2014-07-25 blanchet 2014-07-25 compile
2014-07-25 blanchet 2014-07-25 tuning
2014-07-16 desharna 2014-07-16 generate 'rel_sel' theorem for (co)datatypes
2014-07-16 desharna 2014-07-16 fix rel_cases
2014-07-15 blanchet 2014-07-15 took out 'rel_cases' for now because of failing tactic
2014-07-07 desharna 2014-07-07 refactor some tactics
2014-07-07 desharna 2014-07-07 refactor some tactics
2014-07-07 desharna 2014-07-07 generate 'rel_cases' theorem for (co)datatypes
2014-07-01 desharna 2014-07-01 generate 'rel_induct' theorem for datatypes
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-06-02 desharna 2014-06-02 generate 'sel_set' theorem for (co)datatypes
2014-05-21 desharna 2014-05-21 generate 'sel_map[simp]' theorem for (co)datatypes and tuning 'disc_map_iff'
2014-05-15 desharna 2014-05-15 generate 'disc_map_iff[simp]' theorem for (co)datatypes
2014-05-19 desharna 2014-05-19 fix 'set_empty' theorem when the discriminator is 'op ='
2014-05-12 desharna 2014-05-12 generate 'set_empty' theorem for BNFs
2014-04-28 blanchet 2014-04-28 cleaner 'rel_inject' theorems
2014-03-21 wenzelm 2014-03-21 more qualified names;
2014-03-07 blanchet 2014-03-07 balance tuples that represent curried functions
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 blanchet 2014-03-06 renamed 'map_pair' to 'map_prod'
2014-03-06 blanchet 2014-03-06 renamed 'map_sum' to 'sum_map'
2014-03-06 traytel 2014-03-06 more careful simplification of sets (cf. abf91ebd0820)---yields smaller terms
2014-03-04 blanchet 2014-03-04 simplify sets in BNF composition
2014-03-03 blanchet 2014-03-03 removed obsolete, harmful step in tactic
2014-03-03 blanchet 2014-03-03 rationalized internals
2014-02-25 traytel 2014-02-25 joint work with blanchet: intermediate typedef for the input to fp-operations
2014-02-21 blanchet 2014-02-21 adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
2014-02-12 blanchet 2014-02-12 renamed '{prod,sum,bool,unit}_case' to 'case_...'
2014-01-20 blanchet 2014-01-20 move BNF_LFP up the dependency chain
2014-01-20 blanchet 2014-01-20 adjusted comments
2014-01-20 blanchet 2014-01-20 avoid nested 'Tools' directories