removed experimental encoding for Waldmeister

isabelle update -u control_cartouches;

isabelle update -u control_cartouches;

killed final stops in Sledgehammer and friends

prefer infix operations;

early warning when Sledgehammer finds a proof

refined experimental option of Sledgehammer

File.bash_string operations in ML as in Scala -- exclusively for GNU bash, not perl and not user output;
clarified treatment of whitespace in some bash scripts;

tuned signature -- clarified modules;

--HG--
rename : src/Pure/Concurrent/time_limit.ML => src/Pure/Concurrent/timeout.ML

more canonical names

cleaner generation of metainformation in DFG format and TPTP theory exporter for Sledgehammer

added "!=" (disequality) as a TPTP binary operator, since it pops up in LEO-II proofs

proper check for Windows executables;

tuned signature, in accordance to sortBy in Scala;

tuned signature -- prefer qualified names;

SPASS-Pirate is now called Pirate

--HG--
rename : src/HOL/Tools/ATP/scripts/remote_spass_pirate => src/HOL/Tools/ATP/scripts/remote_pirate

separate module Random;
proper Synchronized.var;

discontinued obsolete Output.urgent_message;

Fixed bug which broke isar proof construction for all ATPs except Waldmeister_new

Some work on the new waldmeister integration

merged minimize and auto_minimize

tuning

default on 'metis' for ATPs if preplaying is disabled

rationalized sorting of facts -- so that preplaying (almost always) coincides with the real thing, preventing odd failures

avoid 'eproof' and 'eproof_ram' scripts if possible (i.e. if 'eprover' can produce reasonable enough proofs for one-liner reconstruction)

speed up MaSh a bit

restored a bit of laziness

honor 'try0' also for one-liners

tuning

eliminated needlessly complex message tail

eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)

rationalized preplaying by eliminating (now superfluous) laziness

simplified minimization logic

use parallel preplay machinery also for one-line proofs

always minimize Sledgehammer results by default

imported patch satallax_proof_support_Sledgehammer

integrated new Waldmeister code with 'sledgehammer' command

fixed parsing of one-argument 'file()' in TSTP files

simplified code

Moving the remote prefix deleting on Sledgehammer's side

add support for Isar reconstruction for thf1 ATP provers like Leo-II.

renamed Sledgehammer options

basic setup for zipperposition prover

tuning

more qualified names;

avoid changing the state's context -- this results in transfer problems later with SMT, and hence preplay tactic failures

properly overwrite replay data from one compression iteration to another

tuning

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

tuned behavior of 'smt' option

made SML/NJ happier

got rid of 'try0' step that is now redundant

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

renamed ML file

--HG--
rename : src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML => src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML

merged 'reconstructors' and 'proof methods'

rationalized threading of 'metis' arguments

tuning

made SML/NJ happier

tuning

compile

refactor large ML file