unused;

more uniform Execution.fork vs. Execution.print; asynchronous Execution.fork_prints, entrusted to Execution.fork management (NB: Command.print_finished is only relevant for persistent print functions);

added Execution.print: accumulate print operations for some command execution, which are applied later and print time; misc tuning;

tuned proofs

Some useful lemmas

tuned comments;

tuned load order;

superseded by (provide_)parse_files;

tuned;

merged

more warnings for recent versions of Poly/ML (see also fe1f6a1707f7);

eliminated dead code;

proper configuration option "ML_print_depth"; proper ML_exception_trace for HOL-TPTP;

removed junk;

clarified options ML_source_trace and ML_exception_trace (NB: the latter needs to be a system option, since the context is sometimes not available, e.g. for 'theory' command);

separate tokenization and language context for SML: no symbols, no antiquotes;

separate "sml" mode, suppress old "ml" mode altogether;

some SML examples;

added command 'SML_file' for Standard ML without Isabelle/ML add-ons;

updated to scala-2.10.4;

cleanup auxiliary proofs for Brouwer fixpoint theorem (removes ~2400 lines)

prove theorems with fixed variables (export afterwards)

generalized theorems about derivatives of limits of sequences of funtions

removed unused 'ax_specification', to give 'specification' a chance to become localized; tuned whitespace;

merged;

merged

proper Sign.full_name to get internal name (like Sign.add_consts);

formal check of user input, avoiding direct references of interal names;