2009-07-21 wenzelm [Tue, 21 Jul 2009 10:24:57 +0200] rev 32094
prefer simultaneous join -- for improved scheduling;
src/Pure/Concurrent/par_list.ML src/Pure/proofterm.ML src/Pure/thm.ML

2009-07-21 wenzelm [Tue, 21 Jul 2009 10:23:16 +0200] rev 32093
tuned dequeu_towards: try immediate tasks before expensive all_preds;
src/Pure/Concurrent/task_queue.ML

2009-07-21 wenzelm [Tue, 21 Jul 2009 01:05:10 +0200] rev 32092
Display.pretty_thm now requires a proper context;
NEWS

2009-07-21 wenzelm [Tue, 21 Jul 2009 01:03:18 +0200] rev 32091
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
src/FOLP/classical.ML src/FOLP/ex/Prolog.ML src/FOLP/simp.ML src/HOL/Import/import.ML src/HOL/Import/proof_kernel.ML src/HOL/Import/shuffler.ML src/HOL/Nominal/nominal_thmdecls.ML src/HOL/Tools/TFL/casesplit.ML src/HOL/Tools/TFL/rules.ML src/HOL/Tools/TFL/tfl.ML src/HOL/Tools/atp_minimal.ML src/HOL/Tools/atp_wrapper.ML src/HOL/Tools/choice_specification.ML src/HOL/Tools/inductive.ML src/HOL/Tools/inductive_codegen.ML src/HOL/Tools/inductive_realizer.ML src/HOL/Tools/lin_arith.ML src/HOL/Tools/meson.ML src/HOL/Tools/metis_tools.ML src/HOL/Tools/recdef.ML src/HOL/Tools/record.ML src/HOL/Tools/res_atp.ML src/HOL/Tools/res_axioms.ML src/HOL/Tools/res_reconstruct.ML src/HOL/Tools/sat_funcs.ML src/HOL/ex/predicate_compile.ML src/Provers/Arith/fast_lin_arith.ML src/Provers/blast.ML src/Provers/classical.ML src/Pure/Isar/args.ML src/Pure/Isar/calculation.ML src/Pure/Isar/code.ML src/Pure/Isar/context_rules.ML src/Pure/Isar/element.ML src/Pure/Isar/isar_cmd.ML src/Pure/Isar/local_defs.ML src/Pure/Isar/method.ML src/Pure/Isar/obtain.ML src/Pure/Isar/proof.ML src/Pure/Isar/proof_display.ML src/Pure/Isar/runtime.ML src/Pure/ProofGeneral/proof_general_pgip.ML src/Pure/Tools/find_theorems.ML src/Pure/old_goals.ML src/Pure/simplifier.ML src/Sequents/prover.ML src/Sequents/simpdata.ML src/Tools/Code/code_preproc.ML src/Tools/Code/code_printer.ML src/Tools/Code/code_thingol.ML ...

2009-07-21 wenzelm [Tue, 21 Jul 2009 00:56:19 +0200] rev 32090
moved ProofContext.pretty_thm to Display.pretty_thm etc.;
explicit old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
removed some very old thm print operations;
src/Pure/Isar/proof_context.ML src/Pure/display.ML

2009-07-20 wenzelm [Mon, 20 Jul 2009 21:20:09 +0200] rev 32089
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
load display.ML after assumption.ML, to accomodate proper contextual theorem display;
src/HOL/Tools/Function/lexicographic_order.ML src/Pure/IsaMakefile src/Pure/Isar/proof.ML src/Pure/Proof/reconstruct.ML src/Pure/ROOT.ML src/Pure/display.ML src/Pure/display_goal.ML src/Pure/goal.ML src/Pure/old_goals.ML src/Pure/tctical.ML

2009-07-20 wenzelm [Mon, 20 Jul 2009 20:03:19 +0200] rev 32088
removed obsolete CVS Ids;
doc-src/IsarRef/showsymbols doc-src/System/Makefile doc-src/System/Thy/Basics.thy doc-src/System/Thy/Interfaces.thy doc-src/System/Thy/Misc.thy doc-src/System/Thy/Presentation.thy doc-src/System/Thy/ROOT.ML doc-src/System/Thy/document/Basics.tex doc-src/System/Thy/document/Interfaces.tex doc-src/System/Thy/document/Misc.tex doc-src/System/Thy/document/Presentation.tex doc-src/System/system.tex

2009-07-20 wenzelm [Mon, 20 Jul 2009 19:58:11 +0200] rev 32087
merged

2009-07-20 haftmann [Mon, 20 Jul 2009 17:14:06 +0200] rev 32086
merged

2009-07-20 haftmann [Mon, 20 Jul 2009 16:11:00 +0200] rev 32085
deftab: only process theorems on demand
src/Pure/codegen.ML