replay_proof optimized: now performs backwards proof search

code reformatted and restructured, many minor modifications

bugfix in "zchaff_with_proofs"

parse_std_result_file renamed to read_std_result_file

new sat tactic

new sat tactic imports resolution proofs from zChaff

fix

simprocs: pattern now "x" (the proc is supposed to discriminate faster than Pattern.match);

tuned msg;

added mk_solver'; export revert_bounds; check_bounds if debug_simp;

Simplifier.inherit_bounds;

adm_tac/cont_tacRs: proper simpset;

Provers/Arith/fast_lin_arith.ML: Simplifier.inherit_bounds;

tuned order of targets;

Provers/cancel_sums.ML: Simplifier.inherit_bounds;

some typos in comments fixed

1) fixed bug in type_introduction: first stage uses different namespace than second stage 2) fixed bug in dump_import_thy via gen2replay function

removed doc/index.html from distribution (now produced by website);

mkdir -p for symlinks

rules -> iprover

spaces inserted in header

header (title/ID) added

typo fixed: rufute -> refute

bugfix in record_tr'

method 'rules' renamed to 'iprover', which does *not* retrieve theorems from the Internet;

Id;

tuned;

changed defaults

ATP linkup

replay type_introduction fix