goal-directed proof now enforces strict proof irrelevance wrt. sort hypotheses;

added translations for SORT_CONSTRAINT tuned;

conclude_goal: precise goal context, include all sorts from context into statement, check shyps of result;

added make;

maintain sort occurrences of declared terms;

added weaken_sorts; strip_shyps: minimal list of minimized extra sorts; tuned;

added make, minimal_sorts;

added const sort_constraint with syntax SORT_CONSTRAINT -- logically vacous;

added check_shyps, which reject pending sort hypotheses;

Drule.norm_hhf_eqs;

prove_common: include all sorts from context into statement, check shyps of result; Drule.norm_hhf_eqs;

added rules for sort_constraint, include in norm_hhf_eqs; tuned;

tuned;

avoid accidental dependency of automated proof on sort equiv;

explicit SORT_CONSTRAINT for proofs depending implicitly on certain sorts;

avoid CRITICAL with_path;

rewrite more proofs in Isar style

Removed ex/Locales.thy.

More occurrences of 'includes' gone.

Removed outdated locales tutorial.

correct rounding

circumvent some TeX problem

only test HOL image for smlnj

tuned;

tuned;

generic ATP manager based on threads (by Fabian Immler);

added sledgehammer etc.;

removed obsolete Complex sessions;

figure for adaption

Removed 'includes' (fixed).

Removed 'includes'.

give more time to do inital loggin and settings read

log start of test session

tuned interfaces -- plain prover function, without thread; misc tuning and simplification; reduced NJ basis library stuff to bare minimum;

add_prover: plain prover function, without thread; removed obsolete atp_thread interface; moved kill_excessive into main thread manager loop -- avoids race condition wrt. register/unregister; start_prover: register/unregister self -- avoids race condition;

tuned AtpWrapper interfaces;

continued codegen tutorial

renamed AtpThread to AtpWrapper;

adding preferences is now permissive;

tuned;

adding preferences is now permissive, no error handling here; tuned messages;

CRITICAL access to preferences; tuned some interfaces;

export generic_pref etc.; CRITICAL access to preferences; misc cleanup, more conventional indentation;

renamed kill_all to kill, in conformance with atp_kill command; simplified/unified treatment of preferences; check_thread_manager: CRITICAL due to global ref; goal addressing via Thm.cprem_of; reduced NJ basis library stuff to bare minimum;

tuned comments;

added lemma

Added liveness analysis

info: back to plain printing; maintain state as Synchronized.var (cf. Pure/Concurrent/synchronized.ML); turned start into check_thread_manager, which forks the managing thread on demand; simplified heap operations; default preferences: only include e prover, which is most likely to be installed; misc simplifcation and tuning;

added min_elem, upto;

added value; simplified synchronized variable access;

simplified synchronized variable access; tuned;

State variables with synchronized access.

added generic combinator for synchronized evaluation (formerly in future.ML);

simplified implementation using Synchronized.var;

SimpleThread.synchronized;

added Concurrent/synchronized.ML;