2016-12-22 haftmann [Thu, 22 Dec 2016 08:43:30 +0100] rev 64634
proper logical constants
NEWS src/HOL/Partial_Function.thy src/HOL/Probability/Probability_Mass_Function.thy src/HOL/Probability/SPMF.thy src/HOL/Relation.thy

2016-12-21 haftmann [Wed, 21 Dec 2016 21:26:26 +0100] rev 64633
prefer existing logical constant over abbreviation
NEWS src/HOL/Relation.thy

2016-12-21 haftmann [Wed, 21 Dec 2016 21:26:26 +0100] rev 64632
dropped aliasses
NEWS src/HOL/Library/Transitive_Closure_Table.thy src/HOL/Relation.thy src/HOL/Wellfounded.thy

2016-12-21 haftmann [Wed, 21 Dec 2016 21:26:25 +0100] rev 64631
removed dangerous simp rule: prime computations can be excessively long
src/HOL/Number_Theory/Factorial_Ring.thy src/HOL/Number_Theory/Gauss.thy

2016-12-20 haftmann [Tue, 20 Dec 2016 15:39:13 +0100] rev 64630
emphasize dedicated rewrite rules for congruences
src/HOL/Divides.thy src/HOL/Statespace/state_fun.ML src/HOL/String.thy

2016-12-21 blanchet [Wed, 21 Dec 2016 17:37:58 +0100] rev 64629
moved and exported tactic
src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML src/HOL/Tools/BNF/bnf_tactics.ML

2016-12-21 blanchet [Wed, 21 Dec 2016 13:35:58 +0100] rev 64628
export ML function (towards nonuniform datatypes)
src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML

2016-12-21 blanchet [Wed, 21 Dec 2016 12:49:15 +0100] rev 64627
generalized ML function (towards nonuniform datatypes)
src/HOL/Tools/BNF/bnf_def.ML src/HOL/Tools/BNF/bnf_fp_def_sugar.ML src/HOL/Tools/BNF/bnf_gfp_grec.ML src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML src/HOL/Tools/BNF/bnf_gfp_grec_sugar_util.ML src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML src/HOL/Tools/BNF/bnf_lfp_countable.ML src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML

2016-12-21 blanchet [Wed, 21 Dec 2016 11:45:16 +0100] rev 64626
generalized ML function (towards nonuniform datatypes)
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML

2016-12-21 blanchet [Wed, 21 Dec 2016 11:14:55 +0100] rev 64625
merge
src/Tools/VSCode/src/line.scala src/Tools/VSCode/src/uri_resources.scala src/Tools/jEdit/src/rendering.scala