more liberal step merging

rationalized lists of methods

extended method list

don't lose additional outcomes

properly overwrite replay data from one compression iteration to another

tuning

merged;

unused;

more formal markup;

clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead; fewer squiggles;

just error, not a failed attempt to raise an exception;

tuned whitespace;

tuned;

generate comments in Isar proofs

allow merging of steps with subproofs

renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover

tuned behavior of 'smt' option

keep all proof methods in data structure until the end, to enhance debugging output

proper fresh name generation

code generation: explicitly declared identifiers gain predence over implicit ones

tuned

tuned storage of code identifiers

searchable underscores

added new option to documentation

added 'smt' option to control generation of 'by smt' proofs

renamed ML file

tuning

merged 'reconstructors' and 'proof methods'

added 'smt' as a proof method

when merging, don't try methods that failed or timed out for either of the steps for the combined step