2011-03-20 wenzelm [Sun, 20 Mar 2011 23:07:06 +0100] rev 42018
modernized specifications;
src/HOL/TLA/Action.thy src/HOL/TLA/Init.thy src/HOL/TLA/Intensional.thy src/HOL/TLA/Memory/MemClerk.thy src/HOL/TLA/Memory/MemClerkParameters.thy src/HOL/TLA/Memory/Memory.thy src/HOL/TLA/Memory/MemoryImplementation.thy src/HOL/TLA/Memory/ProcedureInterface.thy src/HOL/TLA/Memory/RPC.thy src/HOL/TLA/Memory/RPCMemoryParams.thy src/HOL/TLA/Stfun.thy

2011-03-20 wenzelm [Sun, 20 Mar 2011 22:48:08 +0100] rev 42017
dropped unused structure aliases;
src/Pure/ML-Systems/proper_int.ML

2011-03-20 wenzelm [Sun, 20 Mar 2011 22:47:08 +0100] rev 42016
tuned;
src/Pure/Thy/term_style.ML src/Pure/theory.ML

2011-03-20 wenzelm [Sun, 20 Mar 2011 22:26:43 +0100] rev 42015
NEWS: structure Timing provides various operations for timing;
NEWS

2011-03-20 wenzelm [Sun, 20 Mar 2011 22:08:12 +0100] rev 42014
simplified various cpu_time clones (!): eliminated odd Exn.capture/Exn.release (no need to "stop" timing);
src/HOL/Mirabelle/Tools/mirabelle.ML src/HOL/Mutabelle/mutabelle_extra.ML src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML src/Tools/quickcheck.ML

2011-03-20 wenzelm [Sun, 20 Mar 2011 21:44:38 +0100] rev 42013
pure Timing.timing, without any exception handling;
clarified cond_timeit: propagate interrupt without side-effect;
src/Pure/General/timing.ML

2011-03-20 wenzelm [Sun, 20 Mar 2011 21:28:11 +0100] rev 42012
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
explicit Timing.message function;
eliminated Output.timing flag, cf. Toplevel.timing;
tuned;
src/HOL/Matrix/Compute_Oracle/report.ML src/HOL/Mirabelle/Tools/mirabelle.ML src/HOL/Mutabelle/mutabelle_extra.ML src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML src/HOL/ex/SAT_Examples.thy src/Provers/blast.ML src/Pure/General/markup.ML src/Pure/General/output.ML src/Pure/General/timing.ML src/Pure/IsaMakefile src/Pure/Isar/outer_syntax.ML src/Pure/Isar/toplevel.ML src/Pure/ML-Systems/polyml_common.ML src/Pure/ML-Systems/smlnj.ML src/Pure/PIDE/document.ML src/Pure/ProofGeneral/preferences.ML src/Pure/ROOT.ML src/Pure/System/session.ML src/Pure/Tools/find_consts.ML src/Pure/Tools/find_theorems.ML src/Tools/quickcheck.ML

2011-03-20 wenzelm [Sun, 20 Mar 2011 21:20:07 +0100] rev 42011
pervasive cond_timeit;
src/HOL/Tools/Predicate_Compile/mode_inference.ML src/HOL/Tools/Predicate_Compile/predicate_compile.ML src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML

2011-03-20 wenzelm [Sun, 20 Mar 2011 20:20:41 +0100] rev 42010
eliminated dead code;
src/Pure/Thy/present.ML

2011-03-20 wenzelm [Sun, 20 Mar 2011 20:05:43 +0100] rev 42009
parallel preparation of document variants, within separate directories;
doc-src/System/Thy/Presentation.thy doc-src/System/Thy/document/Presentation.tex src/Pure/Thy/present.ML