2015-04-01 wenzelm [Wed, 01 Apr 2015 13:32:32 +0200] rev 59890
tuned signature;
src/Pure/Isar/bundle.ML src/Pure/Isar/isar_syn.ML src/Pure/Isar/local_theory.ML

2015-04-01 wenzelm [Wed, 01 Apr 2015 11:55:23 +0200] rev 59889
tuned message;
src/Pure/General/name_space.ML

2015-04-01 wenzelm [Wed, 01 Apr 2015 10:35:43 +0200] rev 59888
tuned signature;
src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML src/Pure/General/long_name.ML src/Pure/General/name_space.ML src/Pure/Tools/find_theorems.ML

2015-03-31 wenzelm [Tue, 31 Mar 2015 23:42:57 +0200] rev 59887
more visibility flags on background naming;
src/Pure/General/name_space.ML src/Pure/Isar/local_theory.ML

2015-03-31 wenzelm [Tue, 31 Mar 2015 22:31:05 +0200] rev 59886
support for explicit scope of private entries;
src/Pure/General/binding.ML src/Pure/General/name_space.ML src/Pure/Isar/local_theory.ML src/Pure/Isar/proof_context.ML src/Pure/sign.ML

2015-03-31 wenzelm [Tue, 31 Mar 2015 21:12:22 +0200] rev 59885
subtle change of long-standing name space policy: unknown entries are treated as hidden, consequently "private" is understood in the strict sense;
src/Pure/General/binding.ML src/Pure/General/name_space.ML src/Pure/type.ML

2015-03-31 wenzelm [Tue, 31 Mar 2015 20:18:10 +0200] rev 59884
tuned signature;
src/Pure/General/name_space.ML src/Pure/Isar/locale.ML src/Pure/facts.ML src/Pure/thm.ML src/Pure/type.ML src/Pure/variable.ML

2015-03-31 wenzelm [Tue, 31 Mar 2015 20:07:37 +0200] rev 59883
tuned signature;
src/Pure/General/name_space.ML src/Pure/facts.ML src/Pure/variable.ML

2015-03-31 wenzelm [Tue, 31 Mar 2015 19:39:05 +0200] rev 59882
tuned -- avoid exotic Name_Space.defined_entry;
src/HOL/TPTP/TPTP_Proof_Reconstruction.thy

2015-03-31 wenzelm [Tue, 31 Mar 2015 19:16:44 +0200] rev 59881
tuned;
src/Pure/General/name_space.ML