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

2010-12-29 wenzelm [Wed, 29 Dec 2010 12:22:38 +0100] rev 41408
tuned comments;
src/HOL/Mutabelle/mutabelle.ML src/HOL/Mutabelle/mutabelle_extra.ML

2010-12-29 wenzelm [Wed, 29 Dec 2010 12:16:49 +0100] rev 41407
made SML/NJ happy;
more accurate dependencies;
src/HOL/IsaMakefile src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML

2010-12-28 wenzelm [Tue, 28 Dec 2010 18:28:52 +0100] rev 41406
made SML/NJ happy;
src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML

2010-12-27 krauss [Mon, 27 Dec 2010 12:33:21 +0100] rev 41405
function (tailrec) is a legacy feature
src/HOL/Tools/Function/function.ML

2010-12-25 krauss [Sat, 25 Dec 2010 22:18:58 +0100] rev 41404
dropped duplicate unused lemmas;
spelling
src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy