2016-03-18 wenzelm [Fri, 18 Mar 2016 21:29:10 +0100] rev 62673
observe ML print depth;
src/Pure/ML/ml_pp.ML

2016-03-18 wenzelm [Fri, 18 Mar 2016 21:21:09 +0100] rev 62672
clarified print depth;
src/HOL/Metis.thy src/Pure/General/pretty.ML src/Pure/ML/ml_pretty.ML src/Pure/Tools/ml_process.scala

2016-03-18 wenzelm [Fri, 18 Mar 2016 20:35:01 +0100] rev 62671
recovered from Unicode accident in 7248d106c607;
NEWS

2016-03-18 wenzelm [Fri, 18 Mar 2016 20:29:50 +0100] rev 62670
merged
NEWS src/Pure/General/secure.ML src/Pure/General/sha1_polyml.ML src/Pure/General/sha1_samples.ML src/Pure/ML/install_pp_polyml.ML

2016-03-18 wenzelm [Fri, 18 Mar 2016 18:32:35 +0100] rev 62669
tuned -- fewer warnings;
src/Pure/Syntax/parser.ML

2016-03-18 wenzelm [Fri, 18 Mar 2016 17:58:19 +0100] rev 62668
discontinued slightly odd "secure" mode;
src/Pure/General/secure.ML src/Pure/ML/ml_compiler.ML src/Pure/ML/ml_compiler0.ML src/Pure/ROOT src/Pure/ROOT.ML src/Pure/System/isabelle_process.scala src/Pure/Tools/ml_process.scala

2016-03-18 wenzelm [Fri, 18 Mar 2016 17:51:57 +0100] rev 62667
clarified Pretty.T toplevel pp;
src/Pure/General/pretty.ML src/Pure/ML/ml_pp.ML

2016-03-18 wenzelm [Fri, 18 Mar 2016 17:11:30 +0100] rev 62666
clarified modules;
src/Pure/General/sha1.ML src/Pure/General/sha1_polyml.ML src/Pure/General/sha1_samples.ML src/Pure/ROOT src/Pure/ROOT.ML src/Pure/System/isabelle_process.ML src/Pure/Tools/build.ML

2016-03-18 wenzelm [Fri, 18 Mar 2016 16:38:40 +0100] rev 62665
clarified modules;
src/Pure/ML/install_pp_polyml.ML src/Pure/ML/ml_pp.ML src/Pure/ROOT src/Pure/ROOT.ML

2016-03-18 wenzelm [Fri, 18 Mar 2016 16:38:04 +0100] rev 62664
tuned header;
src/Pure/System/bash_windows.ML