2013-10-18 blanchet [Fri, 18 Oct 2013 18:58:46 +0200] rev 54159
set stage for more flexible 'primrec' syntax for recursion through functions
src/HOL/BNF/Tools/bnf_fp_def_sugar.ML src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML src/HOL/BNF/Tools/bnf_fp_util.ML

2013-10-18 blanchet [Fri, 18 Oct 2013 17:47:25 +0200] rev 54158
don't print BNF constants
src/HOL/BNF/Tools/bnf_def.ML

2013-10-18 blanchet [Fri, 18 Oct 2013 16:02:07 +0200] rev 54157
tuning
src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML

2013-10-18 blanchet [Fri, 18 Oct 2013 15:42:55 +0200] rev 54156
conceal even more ugly constructions
src/HOL/BNF/Tools/bnf_def.ML

2013-10-18 blanchet [Fri, 18 Oct 2013 15:25:39 +0200] rev 54155
conceal more ugly constructions
src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML src/HOL/BNF/Tools/ctr_sugar.ML

2013-10-18 blanchet [Fri, 18 Oct 2013 15:19:21 +0200] rev 54154
conceal prim(co)rec definitions
src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML

2013-10-18 blanchet [Fri, 18 Oct 2013 15:12:04 +0200] rev 54153
avoid 'co_' prefix with underscore meaning 'co', since it is our only possible identifier representation of '(co)'
src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML

2013-10-18 blanchet [Fri, 18 Oct 2013 15:00:40 +0200] rev 54152
updated docs
src/Doc/Datatypes/Datatypes.thy

2013-10-18 blanchet [Fri, 18 Oct 2013 14:58:02 +0200] rev 54151
set code attribute on discriminator equations
src/HOL/BNF/Tools/ctr_sugar.ML

2013-10-18 blanchet [Fri, 18 Oct 2013 13:38:55 +0200] rev 54150
MaSh error handling
src/HOL/Tools/Sledgehammer/MaSh/src/mash.py src/HOL/Tools/Sledgehammer/MaSh/src/server.py