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;

added subset operation;

Added fresh_star_const.

Added some more theorems to NominalData.

Added some more lemmas that are useful in proof of strong induction rule.

removed obsolete name convention "func"

fixed typo

clarified function transformator interface

op = vs. eq

moved future_scheduler flag to skip_proof.ML;

added future_scheduler (from thy_info.ML); prove: Goal.prove_promise if future_schedule;

simplified promise; fulfill is internal only; more robust join_futures;

simplified Thm.promise; prove_common: proper context for promise_result;

explicit checkpoint for low-level (global) theory operations admits concurrent SkipProof.prove; tuned list operations;

explicit checkpoint for low-level (global) theory operations, admits concurrent proofs;

circumvent problem with code redundancy

clarifed redundancy policy

tuned comments;

added release_results; tuned comments;

abtract types: plain datatype with opaque signature matching; promise: join pending futures at end of theory;

prove: error with original thread position;

explicit type OrdList.T;

(temporary workaround)

(temporal deactivation)

non left-linear equations for nbe

non left-linear equations for nbe

map_force

matchess

burrow_fst

discontinued special treatment of op = vs. eq_class.eq

report: produce individual status messages;

protocol change: remapped message codes to make room for nested system messages (e.g. for protocol proxy); added Kind.code map;

protocol change: remapped message codes to make room for nested system messages (e.g. for protocol proxy);

init: OuterKeyword.report;

prove_multi: immediate;

added promise_result, prove_promise;

Corrected call of SUBPROOF in coherent_tac that used wrong context.

fixed outer syntax

case default fallback for NBE

fixed quickcheck parameter syntax