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

really unfold

avoid non-standard simp default rule

now covered by AFP 3ddac3e572cf

avoid name shadowing

spelling

predicator simplification rules: support also partially specialized types e.g. 'a * nat

all BNF tests can be part of a normal session because they are much faster now

merged

tuned;

modernized Future/Promise implementation, bypassing old actors;

updated according to scala-2.11.0 recommendations;

explicit Exn.error_message in accordance to Output.error_message in ML;

detect nested interrupts;

clarified message and return code, in accordance to ML version;

interruptible dependencies, which can take a few seconds;

more abstract Exn.Interrupt and POSIX return code;

avoid accidental use of scala.language.reflectiveCalls;

tuned options for scalac;

updated workaround;

avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;

avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;

avoid octal escape literals -- deprecated in scala-2.11.0;

updated to scala-2.11.0 with classpath provided by its etc/settings;

no need to copy jars, after regular use of classpath in 793a429c63e7;

accomodate scala-2.11.0: evade somewhat erratic fix of ImmutableSetFactory in Scala/bfa70315d72d;

made SML/NJ happier

size function for multisets

updated BNF docs

qualify name

tuned doc comment

updated NEWS

localize new size function generation code

no need to make 'size' generation an interpretation -- overkill

put theorems in right slot

manual merge + added 'rel_distincts' field to record for symmetry

pick up all 'nesting' theorems

added 'size' of finite sets

prevent tactic failures by detecting and ignoring BNFs with no 'size' functions early

updated docs

move size hooks together, with new one preceding old one and sharing same theory data

allow registration of custom size functions for BNF-based datatypes

reverted rb458558cbcc2 -- better to keep 'case' and 'rec' distinct, otherwise we lose the connection between 'ctor_rec' (the low-level recursor) and 'rec'

generate 'rec_o_map' and 'size_o_map' in size extension

made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)