quickcheck invokes TimeLimit.timeLimit only in one separate function

added option to Mirabelle Sledgehammer

merged

reverted cs. 0a3fa8fbcdc5 -- motivation is unreconstructable, produces confusion in user space

tuning

fix handling of "fequal" in generated ATP problems -- the bug was visible if "explicit_apply" was on and "singleton_conv" is one of the facts being translated, as it resulted in an arity error in the ATP (e.g., E)

fix path to etc/settings and etc/components in doc

run all provers in blocking mode, even if a proof was already found -- this behavior is less confusing to the user

remove pointless clutter

make minimizer verbose

tuning

automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)

renamed field

added "Z3 as an ATP" support to Sledgehammer locally

remove Z3 wrapper script, which is no longer necessary now that the SMT module generates SMT-LIB compliant files

added experimental "remote_z3_atp", Sutcliffe's TPTP-syntax-aware wrapper for Z3 -- allows to do head-to-head comparison of Sledgehammer's ATP translation and of Sascha's SMT translation

tuned scope of Multithreading.interrupted vs. Multithreading.with_attributes;

merged

changing auto-quickcheck to be considered a non-interactive invocation of quickcheck

discontinued obsolete lib/scripts/polyml-platform;

clarified comment -- ancienct PG 3.7.x is still in use;

discontinued obsolete alias HOL.thy for @{theory HOL} in ML;

prefer polyml-5.2.1 over odd polyml-5.3.0-old;

some shuffling of isatest settings, to ensure coverage of polyml-5.2.1, polyml-5.3.0, polyml-5.4.0, polyml-5.4.1 (SVN), smlnj/110.72;

reverted slightly odd eb5900951702: isatest-doc should work again due to 4b08499b3db1 (polyml-5.3.0 supports proper TimeLimit, as required for HOL-Nitpick-Examples);

merged

available_provers ~> supported_provers (for clarity)

sort E weights

added support for bleeding-edge E weighting function "SymOffsetsWeight"

transformed lie into truth

enable SMT weights and triggers, since they lead to slight improvements according to the Judgment Day suite

improving sum type and option type term constructions for correct presentation in Smallcheck

Explicitly build HOLCF and ZF images. They are not part of the release any more.

added termination lemmas

improving term construction of product types in Smallcheck which enables correct presentation of counterexamples

discontinued support for Poly/ML 5.2, which was the last version without proper multithreading and TimeLimit implementation;

tuned headers;

updated to polyml-5.3.0, which is presently known as the most robust version;

explicit Multithreading.interrupted to ensure that interrupts stay within the boundaries of managed evaluation blocks;

always test/clear Multithreading.interrupted, indepently of thread attributes; tuned;

added Multithreading.interrupted (cf. java.lang.Thread.interrupted);

more robust TimeLimit: make double sure that watchdog has terminated and interrupts received during uninterruptible state are propagated (NB: Thread.testInterrupt requires InterruptSynch in Poly/ML 5.4.0 or earlier);

more tracing information via Par_List.map_name;

clarified bootstrapping of structure TimeLimit;

more scalable collections of tasks, notably for totality of known group members; tuned;

tuned signature; tuned;

merged

prefer p2e before e2p; use measure_unique_Int_stable_vimage;

add auto support for AE_mp

add borel_fubini_integrable; remove unused bijectivity rules for measureable functions

parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;

Task_Queue.update_timing: more precise treatment of interruptibility; Task_Queue.waiting: potentially expensive wait dependencies are subject to trace flag;

Lazy.force_result: more standard treatment of interruptibility, potentially addressing races of exceptions vs. interrupts;

thm_proof: visible fulfill_body only, without joining nested thms -- retain proof irrelevance, which is important for parallel performance;

tuned comments;

clarified Proofterm.proofs_enabled;

explicit is better than implicit;

tuned odd conditional expression;

eliminated slightly odd abstract type Task_Queue.deps; tuned signature; tuned;

merged

Introduction of metis calls and other cosmetic modifications.

merged

avoid ML structure aliases (especially single-letter abbreviations)

making the bash script swipl_version closer to Isabelle's conventional bash scripts

the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; changed syntax for simple_function, simple_integral, positive_integral, integral and RN_deriv. introduced binder variants for simple_integral, positive_integral and integral.

merged

scala serializer adds parentheses around function literals

made SML/NJ happy

term style 'isub': ad-hoc subscripting of variables that end with digits (x1, x23, ...)

refined Task_Queue.dequeue_deps (more incremental);

maintain Task_Queue.group within Task_Queue.task; Task_Queue.dummy_task: id = 0 in accordance to Document.no_id etc.; tuned signature;

tuned comment;

Future.join_results: discontinued post-hoc recording of dynamic dependencies; abstract Task_Queue.deps; tuned signature; tuned;

more informative task timing: some dependency tracking;

refined task timing: joining vs. waiting; tuned;

simplified trace;

more specific Goal.fork_name;

name "passive" tasks (practically lazy values);

tuned trivial cases;

tuned signature; tuned vacous forks;

support named tasks, for improved tracing;

more direct Future.bulk, which potentially reduces overhead for Par_List; tuned signature;

tuned isatest settings;

added basic task timing;

some notes on Cygwin;

more platform hints;

merged

tuned;

back to post-release mode;

removed obsolete test tags;

removed Florian's email from isatest (bounces)

merged

use pre-image measure, instead of image

use AE_mp in AE_conjI proof

tuned proof

merged

moved theorem

restructured theory; tuned proofs

merged

Gauge measure removed

merged

report mutabelle log in mira configuration

back to post-release mode;

delete .elc files unconditionally -- they cause too many incompatibilities;

Added tag Isabelle2011 for changeset 6d736d983d5c

clarified example settings for Proof General;

adhoc patches relative to ProofGeneral-4.1pre101216, which has setprefs working;

more precise stats;

some adhoc patches for ProofGeneral-4.1pre110112;

enforce STIXGeneral, which is preferred by PG 4.1;

default UTF-8 locale, to work with funny base directory (e.g. Chinese);

enforce fonts;

added option -f FONT;

Proof General 4.x interface wrapper;

old Proof General patches;

Added tag isa2011-test3 for changeset 55a45051b220

Tuned definition of sdiv.

CRITICAL markup for critical poking with unsynchronized references;

Replaced smod by standard mod operator to reflect actual behaviour of the SPARK tools.

cancel document execution before editing, to improve reactivity on systems with few cores;