Added nominal_inductive2.ML

added jEdit settings;

tuned usage line;

Isabelle/jEdit interface wrapper.

join results in isolation;

join_results: allow CRITICAL join of finished futures; added singleton join_result;

Future.join_result;

added Future.enabled check;

ThyOutput: export some auxiliary operations;

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

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;

** Update from Fabian ** added remote prover functions;

** Update from Fabian ** reset print mode when producing proof text;

** Update from Fabian ** preferences/provers: separated by white space, avoid low-level char type; sledgehammer command accepts prover list as well; avoid I/O in critical section of AtpManager.info; more systematic synchronization using higher-order combinators; more descriptive errors when atp fails; keep explicitly requested problem files; added remote prover functions; simplified treatment of prover name in diagnostic output; misc tuning and cleanup;

tuned output;

tuned

tuned

change DISTPREFIX to not use yet another filesystem

tuned

tuned

tuned

tuned

`code func` now just `code`

some adaption

using tikz pictures

tuned default rules of (dvd)

replaced str_of by general peek;

extra Poly/ML toplevel pretty printing in ML-Systems/install_pp_polyml.ML;

fixed spelling;

added enabled; removed pseudo-parallel version of profile -- CRITICAL prevents future join;

added enabled;

Multithreading.enabled;

moved future_scheduler flag to Concurrent/ROOT.ML;

added invalidate_group; SimpleThread.interrupt;

added fail-safe interrupt;

subject to Multithreading.enabled; raw_map: join sequentially, less overhead;

future result: Interrupt invalidates group, but pretends success otherwise;

added future_scheduler flag (tmp!), from skip_proofs.ML; added Concurrent/par_list_dummy.ML;

Dummy version of parallel list combinators -- plain sequential evaluation.

added Concurrent/par_list_dummy.ML;

improved performance of skolem cache, due to parallel map; misc tuning, less verbosity;

SimpleThread.interrupt;

report: back to single message;

added section label;

tuned

do logging to MASTERLOG centrally (avoid multiple writers over NFS as this tends to corrupt the log file if not mounted with -sync option which apparently is not the default any more).

removed legacy |>>>

established canonical argument order in SML code generators

established canonical argument order

made SMLNJ happy

less tracing; removed heartbeat thread;

Future.joint_results is already uninterruptible;