2012-09-14 wenzelm [Fri, 14 Sep 2012 21:23:06 +0200] rev 49373
merged

2012-09-14 blanchet [Fri, 14 Sep 2012 12:09:27 +0200] rev 49372
polished the induction
src/HOL/Codatatype/BNF_FP.thy src/HOL/Codatatype/Tools/bnf_fp_sugar.ML src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML

2012-09-14 blanchet [Fri, 14 Sep 2012 12:09:27 +0200] rev 49371
put the flat at the right place (to avoid exceptions)
src/HOL/Codatatype/Tools/bnf_fp_sugar.ML

2012-09-14 blanchet [Fri, 14 Sep 2012 12:09:27 +0200] rev 49370
fixed variable exporting problem
src/HOL/Codatatype/Tools/bnf_fp_sugar.ML src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML

2012-09-14 blanchet [Fri, 14 Sep 2012 12:09:27 +0200] rev 49369
compile
src/HOL/Codatatype/Examples/Stream.thy src/HOL/Codatatype/Examples/TreeFsetI.thy

2012-09-14 blanchet [Fri, 14 Sep 2012 12:09:27 +0200] rev 49368
added induct tactic
src/HOL/Codatatype/BNF_FP.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

2012-09-14 blanchet [Fri, 14 Sep 2012 12:09:27 +0200] rev 49367
tuning
src/HOL/Codatatype/Tools/bnf_fp_sugar.ML

2012-09-14 blanchet [Fri, 14 Sep 2012 12:09:27 +0200] rev 49366
renamed "mk_UnN" to "mk_UnIN"
src/HOL/Codatatype/Tools/bnf_fp_sugar.ML src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML src/HOL/Codatatype/Tools/bnf_util.ML

2012-09-14 blanchet [Fri, 14 Sep 2012 12:09:27 +0200] rev 49365
merged two commands
NEWS src/Doc/Sledgehammer/document/root.tex src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML

2012-09-14 blanchet [Fri, 14 Sep 2012 12:09:27 +0200] rev 49364
allow default values to refer to selector arguments -- this is useful, e.g. for tllist: ttl (TNil x) = TNil x (example by Andreas Lochbihler)
src/HOL/Codatatype/Tools/bnf_wrap.ML