fixed proof

added lemmas

Names of variables in perm_eqs are now chosen more carefully to avoid clashes with name "pi".

- removed test_params from CodegenData (now in Pure/Tools/quickcheck.ML) - improved code unfold preprocessor: now uses one single simpset containing all unfolding rules - got rid of some legacy functions

datatype_codegen now checks name of result type of constructor to avoid problems with overloaded constants such as 0.

run a program in a modified environment;

reactivated HOL-Matrix; minor cleanup;

tuned

filled remaining gaps

added type antiquotation

tuned;

added dep for Concurrent/ROOT.ML;

tuned;

removed Locales;

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