2012-09-04 blanchet [Tue, 04 Sep 2012 16:17:22 +0200] rev 49126
implemented "mk_inject_tac"
src/HOL/Codatatype/Tools/bnf_fp_sugar.ML src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML src/HOL/Codatatype/Tools/bnf_gfp.ML src/HOL/Codatatype/Tools/bnf_lfp.ML

2012-09-04 blanchet [Tue, 04 Sep 2012 15:51:32 +0200] rev 49125
implemented "mk_exhaust_tac"
src/HOL/Codatatype/BNF_Library.thy src/HOL/Codatatype/Tools/bnf_fp_sugar.ML src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML src/HOL/Codatatype/Tools/bnf_fp_util.ML src/HOL/Codatatype/Tools/bnf_gfp.ML src/HOL/Codatatype/Tools/bnf_gfp_util.ML src/HOL/Codatatype/Tools/bnf_lfp.ML src/HOL/Codatatype/Tools/bnf_tactics.ML src/HOL/Codatatype/Tools/bnf_wrap.ML

2012-09-04 blanchet [Tue, 04 Sep 2012 14:21:11 +0200] rev 49124
more work on FP sugar
src/HOL/Codatatype/Tools/bnf_fp_sugar.ML src/HOL/Codatatype/Tools/bnf_gfp.ML src/HOL/Codatatype/Tools/bnf_lfp.ML

2012-09-04 blanchet [Tue, 04 Sep 2012 13:06:41 +0200] rev 49123
more work on sugar + simplify Trueprop + eq idiom everywhere
src/HOL/Codatatype/Codatatype.thy src/HOL/Codatatype/Tools/bnf_comp.ML src/HOL/Codatatype/Tools/bnf_def.ML src/HOL/Codatatype/Tools/bnf_fp_sugar.ML src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML src/HOL/Codatatype/Tools/bnf_gfp.ML src/HOL/Codatatype/Tools/bnf_lfp.ML src/HOL/Codatatype/Tools/bnf_util.ML src/HOL/Codatatype/Tools/bnf_wrap.ML

2012-09-04 blanchet [Tue, 04 Sep 2012 13:05:07 +0200] rev 49122
renamed "disc_exclus" theorem to "disc_exclude"
src/HOL/Codatatype/Tools/bnf_wrap.ML src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML

2012-09-04 blanchet [Tue, 04 Sep 2012 13:05:01 +0200] rev 49121
more work on FP sugar
src/HOL/Codatatype/Tools/bnf_comp.ML src/HOL/Codatatype/Tools/bnf_fp_sugar.ML src/HOL/Codatatype/Tools/bnf_fp_util.ML src/HOL/Codatatype/Tools/bnf_gfp.ML src/HOL/Codatatype/Tools/bnf_gfp_util.ML src/HOL/Codatatype/Tools/bnf_lfp.ML src/HOL/Codatatype/Tools/bnf_wrap.ML

2012-09-04 blanchet [Tue, 04 Sep 2012 13:02:32 +0200] rev 49120
smarter "*" syntax -- fallback on "_" if "*" is impossible
src/HOL/Codatatype/Tools/bnf_wrap.ML

2012-09-04 blanchet [Tue, 04 Sep 2012 13:02:32 +0200] rev 49119
more work on FP sugar
src/HOL/Codatatype/Tools/bnf_fp_sugar.ML src/HOL/Codatatype/Tools/bnf_fp_util.ML src/HOL/Codatatype/Tools/bnf_gfp_util.ML src/HOL/Codatatype/Tools/bnf_util.ML src/HOL/Codatatype/Tools/bnf_wrap.ML

2012-09-04 blanchet [Tue, 04 Sep 2012 13:02:31 +0200] rev 49118
renamed theorem
src/HOL/Codatatype/Tools/bnf_wrap.ML src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML

2012-09-04 blanchet [Tue, 04 Sep 2012 13:02:30 +0200] rev 49117
tuned TODO comment
src/HOL/Codatatype/Tools/bnf_wrap.ML