src/HOL/Codatatype/Tools/bnf_wrap.ML
2012-09-14 blanchet 2012-09-14 allow default values to refer to selector arguments -- this is useful, e.g. for tllist: ttl (TNil x) = TNil x (example by Andreas Lochbihler)
2012-09-12 blanchet 2012-09-12 tuning
2012-09-12 blanchet 2012-09-12 tuning
2012-09-12 blanchet 2012-09-12 added optional qualifiers for constructors and destructors, similarly to the old package
2012-09-12 blanchet 2012-09-12 added attributes to theorems
2012-09-11 blanchet 2012-09-11 support for sort constraints in new (co)data commands
2012-09-11 blanchet 2012-09-11 provide a programmatic interface for FP sugar
2012-09-11 blanchet 2012-09-11 added "defaults" option
2012-09-11 blanchet 2012-09-11 removed wrong "transpose" and ensure "sel" theorems are put in the right order (grouped per selector, in the order in which the selectors appear)
2012-09-11 blanchet 2012-09-11 generate all sel theorems
2012-09-11 blanchet 2012-09-11 allow default values for selectors in low-level "wrap_data" command
2012-09-11 blanchet 2012-09-11 added no_dests option
2012-09-11 blanchet 2012-09-11 tuning
2012-09-10 blanchet 2012-09-10 generate "sel_coiters" and friends
2012-09-10 blanchet 2012-09-10 sanity check
2012-09-10 blanchet 2012-09-10 prevent inconsistent selector types
2012-09-10 blanchet 2012-09-10 minor optimization
2012-09-10 blanchet 2012-09-10 allow same selector name for several constructors
2012-09-10 blanchet 2012-09-10 removed done TODO
2012-09-08 blanchet 2012-09-08 tuning
2012-09-08 blanchet 2012-09-08 define coiterators
2012-09-08 blanchet 2012-09-08 repaired constant types
2012-09-08 blanchet 2012-09-08 tuning
2012-09-08 blanchet 2012-09-08 added high-level recursor, not yet curried
2012-09-05 blanchet 2012-09-05 by default, only generate one discriminator for a two-value datatype
2012-09-05 blanchet 2012-09-05 ported "Misc_Data" to new syntax
2012-09-05 blanchet 2012-09-05 made "mk_case_eq_tac" work in the case where the first constructor is an "alternate" constructor (in which case its discriminator paradoxically starts with a negation)
2012-09-05 blanchet 2012-09-05 tuning (systematic 1-based indices)
2012-09-05 blanchet 2012-09-05 added TODO
2012-09-05 blanchet 2012-09-05 fixed "mk_alternate_disc_def_tac" in the case where the constructors are swapped compared with the common Nil/Cons case
2012-09-05 blanchet 2012-09-05 fixed bug in type instantiation of case theorem
2012-09-05 blanchet 2012-09-05 use empty binding rather than "*" for default
2012-09-05 blanchet 2012-09-05 fixed bugs in one-constructor case
2012-09-04 blanchet 2012-09-04 smoothly handle one-constructor types
2012-09-04 blanchet 2012-09-04 implemented "mk_case_tac" -- and got rid of "cheat_tac"
2012-09-04 blanchet 2012-09-04 define "case" constant
2012-09-04 blanchet 2012-09-04 implemented "mk_exhaust_tac"
2012-09-04 blanchet 2012-09-04 more work on sugar + simplify Trueprop + eq idiom everywhere
2012-09-04 blanchet 2012-09-04 renamed "disc_exclus" theorem to "disc_exclude"
2012-09-04 blanchet 2012-09-04 more work on FP sugar
2012-09-04 blanchet 2012-09-04 smarter "*" syntax -- fallback on "_" if "*" is impossible
2012-09-04 blanchet 2012-09-04 more work on FP sugar
2012-09-04 blanchet 2012-09-04 renamed theorem
2012-09-04 blanchet 2012-09-04 tuned TODO comment
2012-09-04 blanchet 2012-09-04 allow pseudo-definition of is_Cons in terms of is_Nil (and similarly for other two-constructor datatypes)
2012-09-04 blanchet 2012-09-04 allow "*" to indicate no discriminator
2012-09-04 blanchet 2012-09-04 tuned TODOs
2012-09-04 blanchet 2012-09-04 export "wrap" function
2012-09-03 blanchet 2012-09-03 rearrange dependencies
2012-09-03 blanchet 2012-09-03 renamed three BNF/(co)datatype-related commands