improve atomization

fix SInE's error handling + run "vampire" locally if either SPASS or E is missing

added entries

update docs

tuning

parse SNARK proofs

added remote SInE and remote SNARK

no spurious trailing "\n" at the end of Sledgehammer's output

don't get confused by wrong slice

make sure that "add:" doesn't influence the relevance filter too much

tuning of relevance filter

minor cleanup

bound variables can be just as evil as schematic variables and lead to unsound proofs (e.g. "all_bool_eq")

update docs

get rid of "minimize_timeout", now that there's an automatic adaptive timeout mechanism in "minimize"

added "max_relevant_per_iter" option to Sledgehammer

thank Andrei instead of Tanya

fix the relevance filter so that it ignores If, Ex1, Ball, Bex

tuning

reactivated -segprot options, just to make double-sure;

tuned Markup_Tree.+ : slightly more expensive version to rebuild rest avoids crash of RedBlack.scala:120 (version Scala 2.8.0), e.g. on the following input: ML {* fun f x = (x + 1, "aaa") *}

tuned;

tuned signature;

simplified Command.status again, reverting most of e5eed57913d0 (note that more complex information can be represented with full markup reports);

proper range for hyperlinks and tooltips, using original markup information;

tuned signature;

misc tuning and simplification;

renamed Markup_Tree.Node to Text.Info; Markup_Tree.select: body may depend on full Text.Info, including range; tuned;

removed obsolete Markup_Tree.flatten/filter;

Isabelle_Hyperlinks: select relevant information directly from Markup_Tree, without intermediate RefInfo;