src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML
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