src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML
2012-09-15 blanchet 2012-09-15 tuning
2012-09-14 blanchet 2012-09-14 merged two unfold steps
2012-09-14 blanchet 2012-09-14 took out one rotate_tac
2012-09-14 blanchet 2012-09-14 killed spurious rotate_tac; use auto instead of blast
2012-09-14 blanchet 2012-09-14 moved blast tactic to where it is actually needed
2012-09-14 blanchet 2012-09-14 correct generalization to 3 or more mutually recursive datatypes
2012-09-14 blanchet 2012-09-14 provide more guidance, exploiting our knowledge of the goal
2012-09-14 blanchet 2012-09-14 fixed issue with bound variables in prem prems + tuning
2012-09-14 blanchet 2012-09-14 use right version of "mk_UnIN"
2012-09-14 blanchet 2012-09-14 select the right premise in "mk_induct_discharge_prem_prems_tac" instead of relying on backtracking
2012-09-14 blanchet 2012-09-14 tuned code before fixing "mk_induct_discharge_prem_prems_tac"
2012-09-14 blanchet 2012-09-14 polished the induction
2012-09-14 blanchet 2012-09-14 fixed variable exporting problem
2012-09-14 blanchet 2012-09-14 added induct tactic
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-11 blanchet 2012-09-11 finished splitting sum types for corecursors
2012-09-11 blanchet 2012-09-11 first step towards splitting corecursor function arguments into (p, g, h) triples
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 debug
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 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 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 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 some work on coiter tactic
2012-09-08 blanchet 2012-09-08 define corecursors
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-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 fixed "mk_exhaust_tac" for the nth time
2012-09-05 blanchet 2012-09-05 tell "select_prem_tac" not to thin any further premisses -- the "rotate_tac" otherwise confuses it
2012-09-05 blanchet 2012-09-05 don't get confused by extraneous premisses
2012-09-04 blanchet 2012-09-04 fixed some type issues in sugar "exhaust_tac"
2012-09-04 blanchet 2012-09-04 implemented "mk_case_tac" -- and got rid of "cheat_tac"
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 sugar + simplify Trueprop + eq idiom everywhere