sharing of token source with span source;

memoing of forked proofs;

tuned;

removed obsolete argument (cf. 954e9d6782ea);

merged

removed obsolete uses of Local_Theory.restore -- package composition P1 #> P2 no longer requires them due to 57def0b39696: P2 finds the results of P1 in the auxiliary context

merged

tuned

increased stack limits (again, cf. d9cf3520083c and 77c3e74bd954);

explicit change_parser thread, which avoids undirected Future.fork with its tendency towards hundreds of worker threads;

tuned proofs;

retain stderr and include it in syslog, which is buffered and thus increases the chance that users see remains from crashes etc.;

prefer Parser.make_gram over Parser.merge_gram, to approximate n-ary merges on theory import; prefer non-strict lazy over strict future;

recovered structural equality from 9d97bd3c086a, otherwise update_perspective might be issued over and over again, canceling a pending/slow execution;

proper intro? declarations -- NB: elim? indexes on major premise, which is too flexible here and easily leads to inefficiences (cf. a0336f8b6558);

improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory

in a local context, also the free variable case needs to be analysed default tip

speed-up proof;

more abstract datatype stamp, which avoids pointless allocation of mutable cells;

modernized some old-style infix operations, which were left over from the time of ML proof scripts;

simplified -- empty_ss already contains minimal mksimps;

Abstract interpretation is now based uniformly on annotated programs, including a collecting and a small step semantics

tuned;

tuned;