updated CASC instructions + tuning

generalized experimental feature slightly

refined experimental option of Sledgehammer

tuned signature -- clarified modules;

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

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

eliminated Nitpick's pedantic support for 'emdash'

better compliance with TPTP SZS standard

use CVC4 instead of CVC3 at CASC

proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
occasionally clarified use of context;

renamed "pairself" to "apply2", in accordance to @{apply 2};

discontinued obsolete Output.urgent_message;

make TPTP tools work on polymorphic (TFF1) problems as well

treat variables as frees in 'conjecture's

don't generate TPTP THF 'Definition's, because they complicate reconstruction for AgsyHOL and Satallax

compile

basic setup for zipperposition prover

tuning

compile

renamed ML file

--HG--
rename : src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML => src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML

tuned ML file name

--HG--
rename : src/HOL/Tools/Nitpick/nitpick_isar.ML => src/HOL/Tools/Nitpick/nitpick_commands.ML

renamed TFF0/THF0 to three-letter acronyms, in keeping with new TPTP policy

send output of "tptp_translate" to standard output, to simplify Geoff Sutcliffe's life

implemented 'tptp_translate'

type theory is purely value-oriented;

made "completish" mode a bit more complete

tuning -- renamed '_from_' to '_of_' in Sledgehammer

simplifier uses proper Proof.context instead of historic type simpset;

clarified Skip_Proof.cheat_tac: more standard tactic;
clarified Method.cheating: check quick_and_dirty when it is actually applied;

moved Refute to "HOL/Library" to speed up building "Main" even more

--HG--
rename : src/HOL/Refute.thy => src/HOL/Library/Refute.thy
rename : src/HOL/Tools/refute.ML => src/HOL/Library/refute.ML

use metaquantification when possible in Isar proofs

look in current directory first before looking up includes in the TPTP directory, as required by Geoff

renamed experimental option

add missing timeout multiplier

renamed TPTP commands to agree with Sutcliffe's terminology

--HG--
rename : src/HOL/TPTP/lib/Tools/tptp_isabelle_comp => src/HOL/TPTP/lib/Tools/tptp_isabelle
rename : src/HOL/TPTP/lib/Tools/tptp_isabelle_demo => src/HOL/TPTP/lib/Tools/tptp_isabelle_hot

don't use aggressive with HO ATP

make Nitpick's handling of definitions more robust in the face of formulas that don't have the expected format (needed for soundness, cf. RNG100+1)

compile

add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"

export more symbols

split into demo and competitive version

--HG--
rename : src/HOL/TPTP/lib/Tools/tptp_isabelle => src/HOL/TPTP/lib/Tools/tptp_isabelle_demo

use Nitpick as an oracle for finite problems

add extensionality to first-order provers

thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)

move LEO-II closer to the top, for testing

smaller batches, to play safe

tuning

more tweaking of TPTP/CASC setup

further tweaking for Satallax, so that TPTP problems before parsing and after generation are as similar as possible/practical

tuning; no need for relevance filter

more work on TPTP Isabelle and Sledgehammer tactics

more work on CASC setup

tweak TPTP Nitpick's output

smoother handling of conjecture, so that its Skolem constants get displayed in countermodels

handle TPTP definitions as definitions in Nitpick rather than as axioms

get rid of old parser, hopefully for good

added timeout argument to TPTP tools

prepend PWD to relative paths

reintroduced old FOF and CNF parsers, to work around TPTP_Parser failures

remove old TPTP CNF/FOF parser; always use Nik's new parser

tuned SZS status output

started integrating Nik's parser into TPTP command-line tools

implemented "tptp_refute" tool

added problem importer