2010-12-29 krauss [Wed, 29 Dec 2010 21:52:44 +0100] rev 41418
more robust decomposition of simultaneous goals
src/HOL/Tools/Function/induction_schema.ML

2010-12-29 krauss [Wed, 29 Dec 2010 21:52:41 +0100] rev 41417
function (default) is legacy feature
src/HOL/Tools/Function/fun.ML src/HOL/Tools/Function/function.ML src/HOL/Tools/Function/function_common.ML src/HOL/Tools/Function/function_core.ML

2010-12-29 wenzelm [Wed, 29 Dec 2010 21:21:11 +0100] rev 41416
more scalable Symbol_Pos.explode;
src/Pure/General/symbol_pos.ML

2010-12-29 wenzelm [Wed, 29 Dec 2010 20:41:33 +0100] rev 41415
tuned ML toplevel pp for type string: observe depth limit;
src/Pure/ML/install_pp_polyml-5.3.ML src/Pure/ML/ml_syntax.ML src/Pure/pure_setup.ML

2010-12-29 wenzelm [Wed, 29 Dec 2010 18:18:42 +0100] rev 41414
theory loader: implicit load path is considered legacy;
NEWS src/HOL/HOLCF/HOLCF.thy src/HOL/Plain.thy src/Pure/ProofGeneral/proof_general_pgip.ML src/Pure/Thy/thy_load.ML

2010-12-29 wenzelm [Wed, 29 Dec 2010 17:34:41 +0100] rev 41413
explicit file specifications -- avoid secondary load path;
doc-src/Classes/Thy/Setup.thy doc-src/LaTeXsugar/Sugar/ROOT.ML doc-src/LaTeXsugar/Sugar/Sugar.thy doc-src/TutorialI/Sets/Examples.thy src/HOL/Algebra/Divisibility.thy src/HOL/Algebra/Exponent.thy src/HOL/Algebra/Group.thy src/HOL/Algebra/ROOT.ML src/HOL/Auth/Guard/Guard_Shared.thy src/HOL/Auth/ROOT.ML src/HOL/Auth/Smartcard/Smartcard.thy src/HOL/Auth/TLS.thy src/HOL/Decision_Procs/Approximation.thy src/HOL/Decision_Procs/Cooper.thy src/HOL/Decision_Procs/Ferrack.thy src/HOL/Decision_Procs/MIR.thy src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy src/HOL/HOLCF/Bifinite.thy src/HOL/HOLCF/FOCUS/Fstream.thy src/HOL/HOLCF/FOCUS/Fstreams.thy src/HOL/HOLCF/FOCUS/Stream_adm.thy src/HOL/HOLCF/Library/Stream.thy src/HOL/HOLCF/ROOT.ML src/HOL/HOLCF/Universal.thy src/HOL/HOLCF/ex/Dagstuhl.thy src/HOL/HOLCF/ex/Focus_ex.thy src/HOL/Hahn_Banach/Bounds.thy src/HOL/Hahn_Banach/Vector_Space.thy src/HOL/Imperative_HOL/Heap.thy src/HOL/Imperative_HOL/Heap_Monad.thy src/HOL/Imperative_HOL/Overview.thy src/HOL/Imperative_HOL/ROOT.ML src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy src/HOL/Imperative_HOL/ex/SatChecker.thy src/HOL/Imperative_HOL/ex/Sublist.thy src/HOL/Import/HOL4Compat.thy src/HOL/IsaMakefile src/HOL/Isar_Examples/Knaster_Tarski.thy src/HOL/Matrix/ComputeFloat.thy src/HOL/Matrix/LP.thy src/HOL/Matrix/Matrix.thy src/HOL/Metis_Examples/Abstraction.thy src/HOL/Metis_Examples/BigO.thy src/HOL/Metis_Examples/Tarski.thy src/HOL/MicroJava/BV/BVExample.thy src/HOL/MicroJava/DFA/Kildall.thy src/HOL/MicroJava/DFA/Semilat.thy src/HOL/MicroJava/ROOT.ML src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy ...

2010-12-29 wenzelm [Wed, 29 Dec 2010 13:51:17 +0100] rev 41412
check_file: secondary load path is legacy feature;
src/Pure/Thy/thy_load.ML

2010-12-29 wenzelm [Wed, 29 Dec 2010 12:37:15 +0100] rev 41411
share_common_data dummy;
src/Pure/ML-Systems/smlnj.ML

2010-12-29 wenzelm [Wed, 29 Dec 2010 12:34:33 +0100] rev 41410
made SML/NJ happy;
src/HOL/Nitpick_Examples/Mono_Nits.thy

2010-12-29 wenzelm [Wed, 29 Dec 2010 12:25:22 +0100] rev 41409
made SML/NJ happy;
src/HOL/Mutabelle/mutabelle_extra.ML