tuned code

don't rename variables which will be renamed later anyway

normalize skolem argument variable names so that they coincide when taking the conjunction

tuning

tuned comments

deal with E definitions

updated 'compress' docs

cleaner 'compress' option

renamed 'sh_minimize' to 'minimize'; compile;

restored more sorting

tuned terminology (cf. 'isar_proofs' option)

sort facts in minimizer as well

default on 'metis' for ATPs if preplaying is disabled

more informative preplay failures

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

slightly earlier exit from preplaying

honor 'dont_minimize' option when preplaying one-liner proof

Metis is being used to emulate E steps;

updated application of print_tac to take context parameter;

better duplicate detection

normalize conjectures vs. negated conjectures when comparing terms

tweaked 'clone' formula detection

fine-tuned Isar reconstruction, esp. boolean simplifications

centralized boolean simplification so that e.g. LEO-II benefits from it

careful when compressing 'obtains'

better handling of variable names

try to get rid of skolems first

nicer generated variable names

tuning

tuning

no need to 'obtain' variables not in formula

more precise handling of LEO-II skolemization

beware of 'skolem' rules that do not skolemize (e.g. LEO-II)

tuning

peek instead of joining -- is perhaps less risky

export ML function

compile

removed 'metisFT' support in Mirabelle

removed Mirabelle minimization code

modernized Mirabelle (a bit) and made it compile

restored a bit of laziness

reorder quantifiers to ease Z3 skolemization

tuned order of arguments

tuned name context code

tuned whitespace

more rational unskolemizing of names

added appropriate method for skolemization of Z3 steps to the mix

pushing skolems under 'iff' sometimes breaks things further down the proof (as was to be feared)

honor 'try0' also for one-liners

tentatively took out 'fastforce' from the set of tried methods -- it seems to be largely subsumed and is hard to silence

further minimize one-liner

tuning

eliminated needlessly complex message tail

updated NEWS

update documentation after removal of 'min' subcommand

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

rationalized preplaying by eliminating (now superfluous) laziness

removed proof methods as provers from docs

simplified minimization logic

tuning

remove lambda-lifting related assumptions from generated Isar proofs

whitespace tuning

remove YXML formatting when parsing backquoted facts supplied manually to Sledgehammer

generate backquotes without markup, since this confuses preplay; bump up spying version identifier;

simplified tactics slightly

cascading timeout in parallel evaluation, to rapidly find optimum

put faster proof methods first

use parallel preplay machinery also for one-line proofs

updated docs

always minimize Sledgehammer results by default

tuned ML function name

reduced preplay timeout to 1 s

added more proof methods for one-liners

unlift before uncombine, because the definition of a lambda-lifted symbol might have an SK combinator in it (in hybrid encodings)

Improving robustness and indentation corrections.

Skolemization for tmp_ite_elim rule in the SMT solver veriT.

Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.

Whitespace and indentation correction.

Simplifying the labels in the proof of the SMT solver veriT.

Changing ~ into - for unuary minus (not supported by veriT)

imported patch satallax_skolemization_in_tree_part

imported patch hilbert_choice_support

veriT changes for lifted terms, and ite_elim rules.

imported patch satallax_proof_support_Sledgehammer

Basic support for the higher-order ATP Satallax.

Subproofs for the SMT solver veriT.

Basic support for the SMT prover veriT.

removing the '= True' generated by Leo-II.

Skolemization support for leo-II and Zipperposition.

document property 'set_induct'

generate 'set_induct' theorem for codatatypes

also try 'metis' with 'full_types'

header tuning

correctly translate THF functions from terms to types

do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly

back to post-release mode -- after fork point;

tuned;

tuned;

no -optimise -- produces bad bytecode;

output state first -- avoid fluctuation wrt. warnings, errors, etc.;

tuned comment;

updated to polyml-5.5.2-1 which addresses two hard crashes;

updated to cygwin-20140725, which is presumably close to Cygwin 1.7.31-1;

added more functions and lemmas

proper mkdir;

proper option -O;

some reshuffling of Poly/ML version to evade failing tests;

old 'defs' is legacy --- slightly odd side-entry that bypasses regular Local_Theory.define interface;

proper volume name, such that background image is found in /Volumes/Isabelle/.background;

tuned;

tuned message;

setup for drag-and-drop DMG;

merge

reordered provers

compile

faster minimization by not adding facts that are already in the simpset

added missing facts to proof method

don't lose 'minimize' flag before it reaches Isar proof text generation

tuning

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