Tuned L'Hospital

merged

more complete simpset for linear arithmetic to avoid warnings: terms such as (2x + 2y)/2 can then be simplified by the linear arithmetic prover during its proof replay

merged

coinduction method accepts a list of coinduction rules (takes the first matching one)

more robust;

clarified presentation order, according to typical amounts;

present ML timing as well;

Polynomial algebra cleanup (tuned)

Polynomial algebra cleanup

provide index.html; tuned;

cpu time is optional (see Timing.message_resources);

proper display of "_";

clarified options and arguments; tuned;

updated NEWS

optimized parent computation in MaSh

avoid loading MaSh file first time around for higher responsiveness of Sledgehammer

tuned MaSh's metacharacters to avoid needless decoding

optimization in MaSh parsing

tuned ML

removed trailing final stops in Nitpick messages

killed final stops in Sledgehammer and friends

tuned message

tuning punctuation in messages output by Isabelle

tuning whitespace in output syntax

gnuplot presentation similar to former isatest-statistics;

tuned;

statistics from session build output;