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

renamed rtype to typerep

added fold_rev; tuned dest, keys;

added del_node, which is more efficient for sparse graphs;

IntGraph.del_node;

join_results: special case for empty list, works without multithreading;

added dest_deriv, removed external type deriv; misc tuning of internal deriv; more substantial promise/fulfill; promise_ord: reverse order on serial numbers; removed unused is_named; get_name: unfinished proof term;

added conditional add_oracles, keep oracles_of_proof private; added fulfill; removed unused is_named; tuned some table operations;

Thm.proof_of;

Added coherent logic prover.

New prover for coherent logic.

Added setup for coherent logic prover.

Added examples for coherent logic prover.

Examples for coherent logic prover.

made the perm_simp tactic to understand options such as (no_asm)

type thm: fully internal derivation, no longer exported; incorporate former deriv.ML as internal abstract type; added rudimentary promise interface; tuned; added is_named (does not require finished derivation);

added is_finished;

added Promise constructor, which is similar to Oracle but may be replaced later; added promise_proof; export min_proof, mk_min_proof; moved infer_derivs to thm.ML as derive_rule0/1/2; tuned oracles_of_proof; added is_named;

removed deriv.ML which is now incorporated into thm.ML;

added reject_draft;

type thm: fully internal derivation, no longer exported;

generic quickcheck framework

TEMPORARY: make batch run happy

absolute Library path

different session branches for HOL-Plain vs. Plain