2012-04-27 wenzelm [Fri, 27 Apr 2012 22:58:29 +0200] rev 47816
prefer Context_Position.report_generic, which observes is_visible flag and thus reduces number of echos;
src/Pure/Isar/attrib.ML

2012-04-27 wenzelm [Fri, 27 Apr 2012 22:47:30 +0200] rev 47815
clarified signature;
src/HOL/Tools/choice_specification.ML src/HOL/Tools/recdef.ML src/Pure/Isar/attrib.ML src/Pure/Isar/element.ML src/Pure/Isar/isar_cmd.ML src/Pure/Isar/obtain.ML src/Pure/Isar/proof.ML src/Pure/ML/ml_antiquote.ML src/Pure/ML/ml_thms.ML src/ZF/Tools/ind_cases.ML src/ZF/Tools/inductive_package.ML src/ZF/Tools/primrec_package.ML

2012-04-27 wenzelm [Fri, 27 Apr 2012 21:47:47 +0200] rev 47814
avoid spurious warning in invisible context, notably Haftmann-Wenzel sandwich;
src/Pure/config.ML

2012-04-27 wenzelm [Fri, 27 Apr 2012 21:44:44 +0200] rev 47813
made Context_Position independent from Config;
src/Pure/ROOT.ML src/Pure/context_position.ML

2012-04-27 blanchet [Fri, 27 Apr 2012 22:36:27 +0200] rev 47812
use Nitpick as an oracle for finite problems
src/HOL/TPTP/ATP_Problem_Import.thy src/HOL/TPTP/atp_problem_import.ML

2012-04-27 blanchet [Fri, 27 Apr 2012 22:36:27 +0200] rev 47811
add extensionality to first-order provers
src/HOL/TPTP/atp_problem_import.ML

2012-04-27 blanchet [Fri, 27 Apr 2012 22:36:27 +0200] rev 47810
avoid duplicate helpers
src/HOL/Tools/ATP/atp_problem_generate.ML

2012-04-27 wenzelm [Fri, 27 Apr 2012 21:24:30 +0200] rev 47809
mention tools and packages earlier;
NEWS

2012-04-27 wenzelm [Fri, 27 Apr 2012 21:17:35 +0200] rev 47808
tuned;
CONTRIBUTORS

2012-04-27 wenzelm [Fri, 27 Apr 2012 21:13:55 +0200] rev 47807
tuned;
NEWS