2015-01-05 blanchet [Mon, 05 Jan 2015 06:56:15 +0100] rev 59277
documented 'transfer' options to 'prim(co)rec'
src/Doc/Datatypes/Datatypes.thy

2015-01-05 blanchet [Mon, 05 Jan 2015 06:56:15 +0100] rev 59276
tuning
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML src/HOL/Tools/Transfer/transfer_bnf.ML src/HOL/Transfer.thy

2014-12-19 desharna [Fri, 19 Dec 2014 14:06:13 +0100] rev 59275
Add plugin to generate transfer theorem for primrec and primcorec
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML src/HOL/Transfer.thy

2014-12-19 desharna [Fri, 19 Dec 2014 11:20:07 +0100] rev 59274
use proper context in function
src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML

2014-12-19 desharna [Fri, 19 Dec 2014 11:19:14 +0100] rev 59273
document 'disc_eq_case'
src/Doc/Datatypes/Datatypes.thy

2015-01-05 blanchet [Mon, 05 Jan 2015 06:56:15 +0100] rev 59272
tuning
src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML

2014-12-19 desharna [Fri, 19 Dec 2014 11:18:58 +0100] rev 59271
generate 'disc_eq_case' for Ctr_Sugars
src/HOL/Tools/BNF/bnf_util.ML src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML src/HOL/Tools/Old_Datatype/old_datatype_data.ML src/HOL/Tools/record.ML

2015-01-05 blanchet [Mon, 05 Jan 2015 06:56:15 +0100] rev 59270
tuning
src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML

2014-12-19 desharna [Fri, 19 Dec 2014 11:18:23 +0100] rev 59269
remove duplication in tactic
src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML

2014-12-19 desharna [Fri, 19 Dec 2014 11:18:00 +0100] rev 59268
document 'case_distrib'
src/Doc/Datatypes/Datatypes.thy