more complete classical rules for Inf and Sup, modelled after theiry counterparts on Inter and Union (and INF and SUP)

subsumed by existing default simp rules for functions and booleans

tuned

avoid non-standard simp default rule

retired wwwfind

use right set of variables for recursive check

merged

tuned -- potentially more robust;

suppress potential dangerous option (see 1baa5d19ac44);

manager is direct receiver of prover output -- discontinued old performance tuning (329320fc88df, 1baa5d19ac44);

modernized theory setup;

just one default thread pool (which is hardwired to Runtime.availableProcessors);

tuned signature -- separate pool for JFuture tasks, which can be canceled;

prefer Isabelle/Scala operations;

unused;

use Z3 4.3.2 to fix most FIXMEs

added Z3 4.3.2 (unstable) component

updated Z3 version number

use Z3 4.3.2 syntax

subscription as target-specific implementation device

make SML/NJ happier;

merged

updated properties for scala.concurrent.ExecutionContext.Implicits.global (future task farm), similar to Isabelle/ML; removed obsolete properties for old actors;

simplified change_buffer (again, see 937826d702d5): no thread, just timer, rely on asynchronous commands_changed.post;

replaced manager Actor by Consumer_Thread, which is lazy to defer its start to actual Handler init time;

tuned whitespace;

obsolete;

clarified Session.Consumer, with Session.Outlet managed by dispatcher thread; eliminated old actors;

tuned comments;

more robust prover termination;

more explicit checks;

tuned signature;

more uniform warning/error handling, potentially with propagation to send_wait caller;

more careful shutdown (amending f2f53f7046f4);

misc tuning;

obsolete;

converted main session manager to Consumer_Thread: messages need to be consumed immediately, postponed_changes replaces implicit actor mailbox scanning;

simplified commands_changed_buffer (in contrast to a8331fb5c959): rely on better performance of Consumer_Thread/Mailbox and more direct Timer (like session_actor.receiver);

simplified -- prefer Consumer_Thread over Actor;

tuned imports;

support for requests with explicit acknowledgment (and exception propagation);

more robust thread: continue after failure;

clarified command_input: Consumer_Thread;

further robustification wrt. unclear ranges;

allow more control of main loop; more robust is_active test, although thread could terminate at any time;

eliminated pointless output actors; clarified command_input, which already includes thread.join;

more robust shutdown; less ooddities;

consumer thread with unbounded queueing of requests (similar to Message_Channel in ML);

proper signaling after each state update (NB: ML version does this uniformly via timed_access);

added Mailbox, as in ML;

synchronized access, similar to ML version;

tuned signature, in accordance to ML version;

eliminated redundant Volatile;

retain canonical reverse order;

more canonical list operations;

tuned signature in accordance to ML version;

canonical list operations, as in ML; avoid odd mutable data structures;

more uniform synchronized variables;

more unfolding and more folding in size equations, to look more natural in the nested case

reintroduced '...' (nonexhaustive) syntax for SPASS-Pirate