2012-07-27 huffman [Fri, 27 Jul 2012 19:27:21 +0200] rev 48561
move ML functions from nat_arith.ML to Divides.thy, which is the only place they are used
src/HOL/Divides.thy src/HOL/Tools/nat_arith.ML

2012-07-27 huffman [Fri, 27 Jul 2012 17:59:18 +0200] rev 48560
replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms
src/HOL/IsaMakefile src/HOL/Nat.thy src/HOL/Tools/lin_arith.ML src/HOL/Tools/nat_arith.ML src/Provers/Arith/cancel_sums.ML

2012-07-27 huffman [Fri, 27 Jul 2012 17:57:31 +0200] rev 48559
give Nat_Arith simprocs proper name bindings by using simproc_setup
src/HOL/Nat.thy src/HOL/Tools/lin_arith.ML src/HOL/Tools/nat_arith.ML src/HOL/ex/Simproc_Tests.thy

2012-07-27 blanchet [Fri, 27 Jul 2012 17:34:33 +0200] rev 48558
tweaks in preparation for type encoding evaluation
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML src/HOL/Tools/ATP/atp_problem_generate.ML src/HOL/Tools/ATP/atp_systems.ML

2012-07-27 wenzelm [Fri, 27 Jul 2012 16:35:02 +0200] rev 48557
merged

2012-07-27 huffman [Fri, 27 Jul 2012 15:42:39 +0200] rev 48556
replace abel_cancel simprocs with functionally equivalent, but simpler and faster ones
src/HOL/Groups.thy src/HOL/IsaMakefile src/HOL/Tools/abel_cancel.ML src/HOL/Tools/group_cancel.ML src/HOL/Tools/lin_arith.ML src/HOL/ex/Simproc_Tests.thy

2012-07-27 blanchet [Fri, 27 Jul 2012 14:56:37 +0200] rev 48555
nicer Nitpick subscript output in jEdit
src/HOL/Tools/Nitpick/nitpick_util.ML

2012-07-27 wenzelm [Fri, 27 Jul 2012 16:33:32 +0200] rev 48554
no_check for @{setting} antiquotations -- empty values are treated as undefined on Cygwin;
doc-src/antiquote_setup.ML

2012-07-27 wenzelm [Fri, 27 Jul 2012 16:27:26 +0200] rev 48553
proper shell variable;
etc/settings

2012-07-27 wenzelm [Fri, 27 Jul 2012 15:37:48 +0200] rev 48552
actually check return code;
src/Pure/System/build.scala