clarified dependencies between arith tools

separate HOL-Main image

polished code generator setup

added theory antiquotation

tuned comments;

handle _ should be avoided (spurious Interrupt will spoil the game);

added norm_export_morphism;

added exit_global, exit_result, exit_result_global; ProofContext.norm_export_morphism;

LocalTheory.exit_global;

HOL no longer depends on HOL-Plain;

setmp_noncritical;

join earlier promises first;

proper setmp_thread_data for nested execute (cf. join_loop);

promise_result: enforce strictly sequential dependencies, via serial numbers;

do not cvs update for doc test (switching to mercurial, update done outside once and for all)

use mercurial repository for isatest

thread_data: include thread name, export access; more tracing;

setmp_noncritical;

dequeue_towards: return bound for unfinished tasks;

moved release_results to future.ML; get_some: simplified via Future.release_results;

added release_results (formerly in par_list.ML); more informative trace_active; join_results: avoid deadlock via nested SYNCHRONOIZED, more robust active join, less rechecking of tasks;

Future.release_results;

more tracing;

Theory.checkpoint for main operations, admits concurrent proofs;

promise: include check into future body, i.e. joined results are always valid; pending future derivations: shared ref within whole theory body, i.e. end-of-theory joins *all* derivations ever forked from a version of the theory; simplified rep_deriv;

proper transfer of theorems that involve classes being instantiated here;

HOL_USEDIR_OPTIONS no longer applies to HOL-Plain (main HOL is rebuilt from Pure);

eliminated polymorphic equality;