src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
2012-09-14 blanchet 2012-09-14 added induct tactic
2012-09-14 blanchet 2012-09-14 tuning
2012-09-14 blanchet 2012-09-14 renamed "mk_UnN" to "mk_UnIN"
2012-09-14 blanchet 2012-09-14 distinguish between nested and nesting BNFs
2012-09-14 blanchet 2012-09-14 make tactic more robust in the case where "asm_simp_tac" already finishes the job
2012-09-14 blanchet 2012-09-14 derive induction via backward proof, to ensure that the premises are in the right order for constructors like "X x y x" where x and y are mutually recursive
2012-09-12 blanchet 2012-09-12 rough and ready induction
2012-09-12 blanchet 2012-09-12 tuning
2012-09-12 blanchet 2012-09-12 set up things for (co)induction sugar
2012-09-12 blanchet 2012-09-12 tuning
2012-09-12 blanchet 2012-09-12 reuse generated names (they look better + slightly more efficient)
2012-09-12 blanchet 2012-09-12 desambiguate grammar (e.g. for Nil's mixfix ("[]"))
2012-09-12 blanchet 2012-09-12 tuning
2012-09-12 blanchet 2012-09-12 reorganized dependencies so that the sugar does not depend on GFP -- this will be essential for bootstrapping
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 allow defaults for one datatype to involve the constructor of another one in the mutually recursive case
2012-09-11 blanchet 2012-09-11 added "defaults" option
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-11 blanchet 2012-09-11 finished splitting sum types for corecursors
2012-09-11 blanchet 2012-09-11 split sum types in corecursor definition
2012-09-11 blanchet 2012-09-11 first step towards splitting corecursor function arguments into (p, g, h) triples
2012-09-11 blanchet 2012-09-11 reverted "id" change: The problem is rather that the "%c. f c" argument sometimes gets eta-reduced
2012-09-11 blanchet 2012-09-11 generate "id" rather than (%v. v)
2012-09-11 blanchet 2012-09-11 correctly generate sel_coiter and sel_corec theorems
2012-09-10 blanchet 2012-09-10 generate "sel_coiters" and friends
2012-09-10 blanchet 2012-09-10 implemented and use "mk_sum_casesN_balanced"
2012-09-10 blanchet 2012-09-10 fixed general case of "mk_sumEN_balanced"
2012-09-10 blanchet 2012-09-10 fixed base case of "mk_sumEN_balanced"
2012-09-10 blanchet 2012-09-10 avoid type inference + tuning
2012-09-10 blanchet 2012-09-10 use balanced sums for constructors (to gracefully handle 100 constructors or more)
2012-09-10 blanchet 2012-09-10 busted -- let's use more neutral names
2012-09-09 traytel 2012-09-09 full name of a type as key in bnf table
2012-09-09 blanchet 2012-09-09 fixed bug with one-value codatatype "codata 'a dead_foo = A"
2012-09-09 blanchet 2012-09-09 tuning
2012-09-09 blanchet 2012-09-09 fixed and reenabled "corecs" theorems
2012-09-09 blanchet 2012-09-09 fixed and enabled generation of "coiters" theorems, including the recursive case
2012-09-09 blanchet 2012-09-09 reactivated generation of "coiters" theorems
2012-09-09 blanchet 2012-09-09 use map_id, not map_id', to allow better composition
2012-09-08 blanchet 2012-09-08 fixed and enabled iterator/recursor theorems
2012-09-08 blanchet 2012-09-08 oops
2012-09-08 blanchet 2012-09-08 fixed bug with one-value types with phantom type arguments
2012-09-08 blanchet 2012-09-08 imported patch debugging
2012-09-08 blanchet 2012-09-08 renamed xxxBNF to pre_xxx
2012-09-08 blanchet 2012-09-08 fixed handling of map of "fun"
2012-09-08 blanchet 2012-09-08 comment out code that's not ready
2012-09-08 blanchet 2012-09-08 tuning
2012-09-08 blanchet 2012-09-08 construct the right iterator theorem in the recursive case
2012-09-08 blanchet 2012-09-08 some work on coiter tactic
2012-09-08 blanchet 2012-09-08 more sugar on codatatypes
2012-09-08 blanchet 2012-09-08 define corecursors
2012-09-08 blanchet 2012-09-08 define coiterators
2012-09-08 blanchet 2012-09-08 TODO
2012-09-08 blanchet 2012-09-08 tuning
2012-09-08 blanchet 2012-09-08 completed iter/rec proofs
2012-09-08 blanchet 2012-09-08 implemented "mk_iter_or_rec_tac"