added emptiness check predicate and singleton projection

added append_after (tuned version of former insert_after of Seq);

double linking for improved performance of "prev"; misc tuning;

merged

added hard timeout for sledgehammer based on elapsed time (no need to trust ATP's timeout handling); separate Perl script to invoke local ATPs and measure their user time, with proper setup of process groups required by E

Isar.define_command: identify transaction;

updated bib;