src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
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;
2014-03-11 blanchet 2014-03-11 added missing theorems to unfolding set
2014-03-07 blanchet 2014-03-07 tuning
2014-03-07 blanchet 2014-03-07 balance tuples that represent curried functions
2014-03-04 blanchet 2014-03-04 register relator equations as spec rules only for datatypes -- for codatatypes they underspecify the function and are therefore dangerous (e.g. to Nitpick)
2014-03-04 blanchet 2014-03-04 renamed a pair of low-level theorems to have c/dtor in their names (like the others)
2014-03-03 blanchet 2014-03-03 removed (co)iterators from documentation
2014-03-03 blanchet 2014-03-03 rationalized internals
2014-03-03 blanchet 2014-03-03 rationalized internals
2014-03-03 blanchet 2014-03-03 rationalized internals
2014-03-03 blanchet 2014-03-03 rationalized internals
2014-03-03 blanchet 2014-03-03 rationalized internals
2014-03-03 blanchet 2014-03-03 rationalize internals
2014-03-03 blanchet 2014-03-03 optimized simple non-recursive datatypes by reusing 'case' for 'rec' constant
2014-03-03 blanchet 2014-03-03 compile
2014-03-03 blanchet 2014-03-03 repaired argument list to corecursor
2014-03-03 blanchet 2014-03-03 got rid of automatically generated fold constant and theorems (to reduce overhead)
2014-02-25 traytel 2014-02-25 joint work with blanchet: intermediate typedef for the input to fp-operations
2014-02-27 blanchet 2014-02-27 correct most general type for mutual recursion when several identical types are involved
2014-02-23 blanchet 2014-02-23 added explicit killing
2014-02-23 blanchet 2014-02-23 more precise error message
2014-02-23 blanchet 2014-02-23 reuse same parser for '(co)datatype(_new)' as for 'bnf_decl'
2014-02-19 blanchet 2014-02-19 moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
2014-02-19 blanchet 2014-02-19 tuning
2014-02-18 blanchet 2014-02-18 prepare two-stage 'primrec' setup
2014-02-18 blanchet 2014-02-18 tuning
2014-02-17 blanchet 2014-02-17 simplified data structure by reducing the incidence of clumsy indices
2014-02-17 blanchet 2014-02-17 name derivations in 'primrec' for code extraction from proof terms
2014-02-14 blanchet 2014-02-14 generate proper 'DtRec' indices in 'datatype_new_compat' for the case where some types are duplicated
2014-02-14 blanchet 2014-02-14 tuned code to allow mutualized corecursion through different functions with the same target type