2014-03-15 wenzelm [Sat, 15 Mar 2014 16:54:32 +0100] rev 56165
tuned markup;
src/Pure/Tools/rail.ML

2014-03-15 wenzelm [Sat, 15 Mar 2014 15:50:41 +0100] rev 56164
minor tuning;
src/Pure/General/name_space.ML

2014-03-15 wenzelm [Sat, 15 Mar 2014 15:49:23 +0100] rev 56163
more markup;
src/Pure/Tools/rail.ML

2014-03-15 wenzelm [Sat, 15 Mar 2014 12:51:14 +0100] rev 56162
clarified completion ordering: prefer local names;
src/Pure/General/completion.scala src/Pure/General/long_name.ML src/Pure/General/name_space.ML

2014-03-15 wenzelm [Sat, 15 Mar 2014 11:59:18 +0100] rev 56161
tuned signature;
eliminated clones;
src/HOL/Mirabelle/Tools/mirabelle.ML src/HOL/Mutabelle/mutabelle.ML src/HOL/Mutabelle/mutabelle_extra.ML src/HOL/Tools/Nitpick/nitpick_hol.ML src/HOL/Tools/Quickcheck/find_unused_assms.ML src/Pure/Proof/proof_checker.ML src/Pure/Proof/proof_syntax.ML src/Pure/global_theory.ML

2014-03-15 wenzelm [Sat, 15 Mar 2014 11:57:55 +0100] rev 56160
tuned -- avoid vacuous reports;
src/Pure/General/name_space.ML

2014-03-15 wenzelm [Sat, 15 Mar 2014 11:28:07 +0100] rev 56159
clarified local facts;
src/Pure/Tools/find_theorems.ML

2014-03-15 wenzelm [Sat, 15 Mar 2014 11:22:25 +0100] rev 56158
more explicit treatment of verbose mode, which includes concealed entries;
src/Doc/IsarRef/Misc.thy src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML src/Pure/Isar/isar_cmd.ML src/Pure/Isar/isar_syn.ML src/Pure/Isar/proof_context.ML src/Pure/Isar/proof_display.ML src/Pure/Tools/find_theorems.ML src/Pure/Tools/proof_general.ML src/Pure/facts.ML

2014-03-15 wenzelm [Sat, 15 Mar 2014 10:29:42 +0100] rev 56157
removed dead code;
src/HOL/Mutabelle/Mutabelle.thy

2014-03-15 wenzelm [Sat, 15 Mar 2014 10:24:49 +0100] rev 56156
clarified retrieve_generic: local error takes precedence, which is relevant for completion;
src/Pure/Isar/proof_context.ML