src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
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"
2012-09-08 blanchet 2012-09-08 generate iter/rec goals
2012-09-08 blanchet 2012-09-08 repaired constant types
2012-09-08 blanchet 2012-09-08 some work towards iterator and recursor properties
2012-09-08 blanchet 2012-09-08 tuning
2012-09-08 blanchet 2012-09-08 correctly curry recursor arguments
2012-09-08 blanchet 2012-09-08 added high-level recursor, not yet curried
2012-09-06 blanchet 2012-09-06 gracefully handle shadowing case (fourth step of sugar localization)
2012-09-06 blanchet 2012-09-06 careful about constructor types w.r.t. fake context (third step of localization)
2012-09-06 blanchet 2012-09-06 read the real types off the constant types, rather than using the fake parser types (second step of sugar localization)
2012-09-06 blanchet 2012-09-06 tuning
2012-09-06 blanchet 2012-09-06 use "add_type" rather than "add_types_global"
2012-09-06 blanchet 2012-09-06 don't throw away the context when hacking the theory (first step to localize the sugar code)
2012-09-06 blanchet 2012-09-06 introduced and used "mk_Freesss", and simplified "mk_Freess(')"
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 blanchet 2012-09-05 print timing information
2012-09-05 blanchet 2012-09-05 check type variables on rhs
2012-09-05 blanchet 2012-09-05 fixed (n + 1)st bug in "mk_exhaust_tac" -- arose with uncurried constructors
2012-09-05 blanchet 2012-09-05 ported "Misc_Data" to new syntax
2012-09-05 blanchet 2012-09-05 added a check
2012-09-04 blanchet 2012-09-04 fixed some type issues in sugar "exhaust_tac"
2012-09-04 blanchet 2012-09-04 optionally provide extra dead variables to the FP constructions
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_half_distinct_tac"
2012-09-04 blanchet 2012-09-04 implemented "mk_inject_tac"
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 sugar + simplify Trueprop + eq idiom everywhere
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-04 blanchet 2012-09-04 started work on sugared "(co)data" commands