src/HOL/Codatatype/Tools/bnf_fp_util.ML
2012-09-10 blanchet 2012-09-10 use balanced sums for constructors (to gracefully handle 100 constructors or more)
2012-09-10 traytel 2012-09-10 stabilized generation of parameterized theorem
2012-09-09 blanchet 2012-09-09 generate "fld_unf_corecs" as well
2012-09-09 traytel 2012-09-09 open typedefs everywhere in the package
2012-09-08 blanchet 2012-09-08 fixed and enabled iterator/recursor theorems
2012-09-08 blanchet 2012-09-08 renamed for consistency
2012-09-08 blanchet 2012-09-08 tuning
2012-09-08 blanchet 2012-09-08 for compatiblity with old datatype package: not only "recs" with "s", but also "iters" and their "fld_"/"unf_" variants
2012-09-08 blanchet 2012-09-08 renamed xxxBNF to pre_xxx
2012-09-08 blanchet 2012-09-08 completed iter/rec proofs
2012-09-08 blanchet 2012-09-08 correctly curry recursor arguments
2012-09-06 traytel 2012-09-06 respect order of/additional type variables supplied by the user in fixed point constructions;
2012-09-06 blanchet 2012-09-06 construct high-level iterator RHS
2012-09-05 blanchet 2012-09-05 honor mixfix specifications
2012-09-05 traytel 2012-09-05 error message only in case of an error
2012-09-05 blanchet 2012-09-05 added comment for Dmitriy
2012-09-04 blanchet 2012-09-04 optionally provide extra dead variables to the FP constructions
2012-09-04 blanchet 2012-09-04 added robustness
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 renamed low-level (co)iterators and (co)recursors with "fld_"/"unf_" prefix
2012-09-04 blanchet 2012-09-04 implemented "mk_exhaust_tac"
2012-09-04 blanchet 2012-09-04 more work on FP sugar
2012-09-04 blanchet 2012-09-04 more work on FP sugar
2012-09-03 blanchet 2012-09-03 rearrange dependencies
2012-08-30 blanchet 2012-08-30 more work on BNF sugar -- up to derivation of nchotomy
2012-08-30 blanchet 2012-08-30 more work on BNF sugar
2012-08-28 blanchet 2012-08-28 added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)