2013-12-12 wenzelm [Thu, 12 Dec 2013 22:38:25 +0100] rev 54731
clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
src/Pure/Tools/simplifier_trace.ML src/Pure/raw_simplifier.ML src/Pure/simplifier.ML

2013-12-12 wenzelm [Thu, 12 Dec 2013 21:28:13 +0100] rev 54730
skeleton for Simplifier trace by Lars Hupel;
src/Pure/Pure.thy src/Pure/Tools/simplifier_trace.ML src/Pure/Tools/simplifier_trace.scala src/Pure/build-jars

2013-12-12 wenzelm [Thu, 12 Dec 2013 21:14:33 +0100] rev 54729
generic trace operations for main steps of Simplifier;
src/Pure/raw_simplifier.ML src/Pure/simplifier.ML

2013-12-12 wenzelm [Thu, 12 Dec 2013 17:34:50 +0100] rev 54728
tuned signature;
src/Pure/raw_simplifier.ML src/Pure/simplifier.ML

2013-12-12 wenzelm [Thu, 12 Dec 2013 16:56:53 +0100] rev 54727
tuned whitespace;
src/Pure/raw_simplifier.ML

2013-12-12 wenzelm [Thu, 12 Dec 2013 16:25:21 +0100] rev 54726
added missing file (cf. 124432e77ecf);
src/Pure/ML-Systems/polyml-5.5.2.ML

2013-12-12 wenzelm [Thu, 12 Dec 2013 16:17:35 +0100] rev 54725
tuned whitespace;
src/Pure/raw_simplifier.ML

2013-12-12 wenzelm [Thu, 12 Dec 2013 14:35:31 +0100] rev 54724
removed dead code -- ctxt is never visible (see also 658fcba35ed7);
src/Pure/raw_simplifier.ML

2013-12-12 wenzelm [Thu, 12 Dec 2013 13:50:44 +0100] rev 54723
simplified polyml-5.5.2 setup -- implicit upgrade of Thread.numProcessors;
src/Pure/ML-Systems/multithreading_polyml.ML src/Pure/ML-Systems/polyml.ML src/Pure/ML-Systems/thread_physical_processors.ML src/Pure/ROOT

2013-12-12 wenzelm [Thu, 12 Dec 2013 13:23:23 +0100] rev 54722
tuned message;
src/Pure/Thy/thy_info.ML src/Pure/Thy/thy_info.scala