src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
2014-08-18 blanchet 2014-08-18 reordered some (co)datatype property names for more consistency
2014-08-14 desharna 2014-08-14 generate 'rel_map' theorem for BNFs
2014-08-12 blanchet 2014-08-12 avoid needless (and wrong w.r.t. sorts) generation of type variables; tuned whitespaces;
2014-08-12 desharna 2014-08-12 generate 'set_cases' theorem for (co)datatypes
2014-08-12 desharna 2014-08-12 generate 'set_intros' theorem for (co)datatypes
2014-08-11 traytel 2014-08-11 use Goal.prove_sorry instead of Goal.prove where possible (= no schematics in goal and tactic is expected to succeed)
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-30 blanchet 2014-07-30 correctly resolve selector names in default value equations
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 tuning
2014-07-24 blanchet 2014-07-24 tuned code
2014-07-24 blanchet 2014-07-24 repaired named derivations
2014-07-24 blanchet 2014-07-24 use the noted theorem whenever possible, also in 'BNF_Def'
2014-07-17 desharna 2014-07-17 fix bug caused by bad context
2014-07-17 desharna 2014-07-17 add mk_Trueprop_mem utility function
2014-07-16 desharna 2014-07-16 refactor commonly used functions
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-09 blanchet 2014-07-09 made SML/NJ happier
2014-07-07 desharna 2014-07-07 generate 'rel_cases' theorem for (co)datatypes
2014-07-03 desharna 2014-07-03 generate 'rel_intros' theorem for (co)datatypes
2014-07-02 desharna 2014-07-02 generate 'corec_code' theorem for codatatypes
2014-07-01 desharna 2014-07-01 generate 'rel_induct' theorem for datatypes
2014-06-27 blanchet 2014-06-27 compile
2014-06-27 blanchet 2014-06-27 tuned variable names
2014-06-24 desharna 2014-06-24 tune the implementation of 'rel_coinduct'
2014-06-24 desharna 2014-06-24 generate 'rel_coinduct' theorem for codatatypes
2014-06-24 desharna 2014-06-24 generate 'rel_coinduct0' theorem for codatatypes
2014-06-18 blanchet 2014-06-18 made tactic more robust in the face of 'primcorec' specifications containing 'case_sum'
2014-06-16 blanchet 2014-06-16 fixed postprocessing of 'coinduct' formula to obtain right property format (without needless hypotheses)
2014-06-10 blanchet 2014-06-10 changed syntax of map: and rel: arguments to BNF-based datatypes
2014-06-10 blanchet 2014-06-10 tuning
2014-06-10 blanchet 2014-06-10 use 'where' clause for selector default value syntax
2014-06-10 blanchet 2014-06-10 tuning
2014-06-02 desharna 2014-06-02 generate 'sel_set' theorem for (co)datatypes
2014-05-27 blanchet 2014-05-27 don't generate discriminators and selectors for 'datatype_new' unless the user asked for it
2014-05-26 blanchet 2014-05-26 got rid of '=:' squiggly
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-16 blanchet 2014-05-16 proper handling of 'ctor_dtor' for mutual corecursive cases where not all type variables are present in all low-level constructors (cf. 'coind_wit1' etc. in 'Misc_Codatatypes.thy')
2014-05-12 desharna 2014-05-12 generate 'set_empty' theorem for BNFs
2014-04-28 blanchet 2014-04-28 restored naming trick
2014-04-28 blanchet 2014-04-28 cleaner 'rel_inject' theorems
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 no need to make 'size' generation an interpretation -- overkill
2014-04-23 blanchet 2014-04-23 manual merge + added 'rel_distincts' field to record for symmetry
2014-04-23 blanchet 2014-04-23 reverted rb458558cbcc2 -- better to keep 'case' and 'rec' distinct, otherwise we lose the connection between 'ctor_rec' (the low-level recursor) and 'rec'
2014-04-23 blanchet 2014-04-23 generate 'rec_o_map' and 'size_o_map' in size extension
2014-04-23 blanchet 2014-04-23 generate size instances for new-style datatypes
2014-04-23 blanchet 2014-04-23 invoke 'fp_sugar' interpretation hook on mutually recursive clique
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-10 kuncar 2014-04-10 export theorems
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 new-style (co)datatype interpretation hook
2014-03-22 wenzelm 2014-03-22 more antiquotations;