discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;

discontinued obsolete 'uses' within theory header;

use lemma from Big_Operators

add inclusion/exclusion lemma

added lemma

merged

add wellorder instance for Numeral_Type (suggested by Jesus Aransay)

updated Toplevel.command_exception;

tuned;

tuned signature;

fork diagnostic commands (theory loader and PIDE interaction); explicit id for load_thy, for more robust Goal.fork accounting and commit for each theory -- NB: use_thys nodes become subject to Position.is_reported like PIDE document transactions; clarified Toplevel.command_exception vs. Toplevel.command_errors;

disallow shutdown from worker, which would lead to deadlock since the scheduler cannot terminate;

tuned 2464ba6e6fc9 -- NB: approximative_id is NONE for PIDE document transactions;

signal work_available should be sufficient to initiate daisy-chained workers, and lead to separate broadcast work_finished eventually -- NB: broadcasting all worker threads tends to burn parallel CPU cycles;

less eventful shutdown: merely wait for scheduler to terminate;

tuned messages;

tuned;

merged;

more explicit Goal.shutdown_futures;

reconsider 'export_code' as "thy_decl" command due to its global side-effect on the file-system;

discontinued pointless command category "thy_schematic_goal" -- this is checked dynamically;

clarified Toplevel.element_result: scheduling policies happen here; tuned;

prefer stateless 'ML_val' for tests;

tuned comment;

reconsider 'pretty_setmargin' as "control" command (instead of "diag") -- it is stateful and Proof General legacy;

merged;

simplified Outer_Syntax.read_span: internalized Toplevel.is_ignored; eliminated separate Outer_Syntax.read_element;

tuned;

unified Command.is_proper in ML with Scala (see also 123be08eed88);

tuned order of modules;

fixed document;

turned example into library for comparing growth of functions

corrected reference

improved orderings

tuned agressiveness of isar compression

eliminated isize in favour of size + type coercion

make SML/NJ happy;

basic setup for appbundler-1.0 for Mac OS X and Java 7;

more robust handling of repeated interrupts while terminating managed process; NB: InterruptedException should have interrupted status cleared already;

more friendly message for spurious InterruptedException, which might still occur due to JVM oddities;

more explicit GUI components for dynamic actions;

clarified Progress.stopped: rising edge only; also cancel jobs that have not been considered yet;

more explicit console interrupt handling;

more permissive File.read_lines, which is relevant for Managed_Process join/kill;

support for POSIX interrupts (bypassed on Windows);

merged

tuned error messages

Coercion_Examples defines required coercions itself (no Complex_Main needed)

apply unifying substitution before building the constraint graph

more abstract intervals

more robust load_timings: ignore XML.Decode errors as well;

make SML/NJ happy;

identify exceptions more robustly, to allow SML/NJ report toplevel errors without crash;

make SML/NJ happy;

updated headers;

eliminated hard tabs;

discontinued obsolete src/HOL/IsaMakefile;

merged

more explicit session dependency, for improved parallel performance of HOL-UNITY test session -- NB: separate 'theories' sections are sequential;

merged

removed obsolete tags;

highest priority for proofs with unknown / very short timing -- recover original scheduling with parallel_proofs_reuse_timing = false;

tuned misleading message

merged

option parallel_proofs_reuse_timing controls reuse of log information -- since it is not always beneficial for performance;

prefer outdegree in comparison again (cf. 88c96e836ed6) -- NB: big jobs might hide behind small ones in this naive queuing scheme;

more tight representation of command timing; tuned signatures; tuned;

prefer comparison of session timing, if this is known already; some odd workarounds to prevent crashes due to TreeSet.- sometimes not deleting the element;

proper check of Proof.is_relevant (again, cf. c3e99efacb67 and df8fc0567a3d);

support nested Thy_Syntax.element; more explicit Keyword.is_proof_body; tuned;

back to non-schematic 'sublocale' and 'interpretation' (despite df8fc0567a3d) for more potential parallelism;

help JVM to cope with large symbolic structures;

improved scheduling of forked proofs, based on elapsed time estimate (from last run via session log file);

read logs from failed sessions as well; proper output base directory (which is two steps upwards);

recover timing information from old log files; use session timing for queue ordering; pass command timings to ML process (still unused);

suppress timing message in full PIDE protocol -- this is for batch build;

support for build passing timings from Scala to ML;

support for prescient timing information within command transactions;

emit command_timing properties into build log; tuned;

generate Isar proof if Metis appears to be too slow

swap slices so that the last slice is more complete (for minimization)

tuning

ensure all conjecture clauses are in the graph -- to prevent exceptions later

generalize syntax of SPASS proofs

tweaked hack some more

more simplifying constructors

remove needless steps from refutation graph -- these confuse the proof redirection algorithm (and are needless)

more precise error

improved hack

upgraded to Alt-Ergo 0.95

don't pass chained facts directly to SMT solvers -- this breaks various invariants and is never necessary

trust preplayed proof in Mirabelle

added case taken out by mistake

tuning (removed redundant datatype)

minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay

honor linearization option also in the evaluation driver

got rid of rump support for Vampire definitions

optimize Isar output some more

turn off more evil Vampire options to facilitate Isar proof generation

fixed typo in option name

tuning

use new skolemizer only if some skolems have two or more arguments -- otherwise the old skolemizer cannot get the arg order wrong

slacker comparison for Skolems, to avoid trivial equations

auto-minimizer should respect "isar_proofs = true"

made "isar_proofs" a 3-way option, to provide a way to totally disable isar_proofs if desired

alias for people like me

dropped spurious left-over from 0a2371e7ced3

avoid using "smt" for minimization -- better use the prover itself, since then Sledgehammer gets to try metis again and gives the opportunity to output an Isar proof -- and show Isar proof as fallback for SMT proofs

interpret "max_facts" argument in a slice-dependent fashion, instead of forcing the same number of facts to all slices

delete also predicates on relations when hiding an implementation of an abstract type

reintroduced crucial sorting accidentally lost in 962190eab40d

compile

provide two modes for MaSh driver: linearized or real visibility

implement (more) accurate computation of parents

tuning

split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations

simplified byline, isar_qualifier

tuned code: factored out parent computation

tuned code

simplify definition as sort constraints ensure finiteness (thanks to Jesus Aransay)