2010-08-27 haftmann [Fri, 27 Aug 2010 13:32:05 +0200] rev 38809
proper namespace administration for hierarchical modules
src/Tools/Code/code_scala.ML

2010-08-27 wenzelm [Fri, 27 Aug 2010 17:59:40 +0200] rev 38808
more antiquotations;
src/HOL/Matrix/Compute_Oracle/compute.ML src/HOL/Nominal/nominal_thmdecls.ML src/HOL/String.thy src/HOL/Tools/Qelim/cooper.ML src/HOL/Tools/SMT/smt_solver.ML

2010-08-27 wenzelm [Fri, 27 Aug 2010 17:23:57 +0200] rev 38807
eliminated Unsynchronized.ref in favour of configuration option;
proper naming of thy: theory vs. ctxt: Proof.context;
recovered some Isabelle/ML indendation style;
src/HOL/Nominal/nominal_thmdecls.ML

2010-08-27 wenzelm [Fri, 27 Aug 2010 17:11:29 +0200] rev 38806
more appropriate name for configuration option "meson_max_clauses" (cf. output of 'pront_configs');
src/HOL/Tools/meson.ML

2010-08-27 wenzelm [Fri, 27 Aug 2010 17:09:18 +0200] rev 38805
Sum_Of_Squares: proper configuration options;
src/HOL/Library/Sum_Of_Squares.thy src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML

2010-08-27 wenzelm [Fri, 27 Aug 2010 17:02:19 +0200] rev 38804
tuned printed type names, according to ML;
src/Pure/config.ML

2010-08-27 wenzelm [Fri, 27 Aug 2010 16:32:11 +0200] rev 38803
eliminated unnecessary ref;
src/HOL/Import/import_syntax.ML

2010-08-27 wenzelm [Fri, 27 Aug 2010 16:29:12 +0200] rev 38802
clarified iter_deepen_limit vs meson (cf. 7c5896919eb8) -- eliminated global ref;
src/HOL/Tools/meson.ML src/Pure/search.ML

2010-08-27 wenzelm [Fri, 27 Aug 2010 15:46:08 +0200] rev 38801
disposed some old debugging tools;
src/HOL/Library/positivstellensatz.ML src/HOL/Tools/TFL/rules.ML

2010-08-27 wenzelm [Fri, 27 Aug 2010 15:07:35 +0200] rev 38800
proper configuration option "show_proofs";
modernized syntax translation;
src/FOLP/IFOLP.thy