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)

compile

more robustness in Isar proof construction

tuning

merged

more elementary exception handling: evade hard crash of (Runtime.thread true undefined) on Poly/ML 5.5.1 and 5.5.2;

tuned code

having extra assumptions (typically from a context) means there is no chance to have a valid code equation => skip decoding and registration of the code equations

store explicitly quotient types with no_code => more precise registration of code equations

don't needlessly regenerate entire file when the time stamps are equal

eliminated source of 'DUP's in MaSh

fixed sorting (broken since 9cc802a8ab06)

reenabled MaSh for Isabelle2014 release (hopefully)

beware of duplicate fact names

refined filter for ATP steps to avoid 'have True' steps in E proofs

filter out 'theory(...)' from dependencies early on

introduce fact chaining also under first step

'shift_quantors' is not an E skolemization rule (cf. 3ab503b04bdb)

merged

proper perl;

less warnings -- ignore potential prover startup/shutdown races;

tuned spelling;

further distinction of Isabelle distribution: alert for identified release candidates;

updated to scala-2.11.2;

clarified file names;

less ambitious isatest, avoid "Exception- InternalError: Backing up too far (32bit) raised while compiling" in polyml-5.4.1;

tuned imports;

proper scope of comments;

make SML/NJ happy;

prevent beta-contraction in proving extra assumptions for abs_eq

more robust notation BNF_Def.convol, which is private to main HOL, but may cause syntax ambiguities nonetheless (e.g. List.thy);

reconfirm continuous checking on startup, to address common trap of disabling it accidentally;

tuned;

less authentic SHA1.digest: trust Scala side on blobs and avoid re-calculation via Foreign Language Interface, which might be a cause of problems;

updated NEWS according to d38a98f496dd (see also bdc2c6b40bf2);

stick to external proofs when invoking E, because they are more detailed and do not merge steps

more robust handling of types for skolems (modeled as Frees)

tuning

repaired named derivations

use the noted theorems in 'BNF_Comp'

use the noted theorem whenever possible, also in 'BNF_Def'

use termtab instead of (perhaps overly sensitive) thmtab

use the noted theorem whenever possible, because it has a named derivation (leading to cleaner proof terms)

tuned message;

added action "isabelle.options" (despite problems with initial window size);

more official Thy_Info.script_thy;

more frugal edits;

enable hires explictly, as seen for other high-end Java applications on the Web;

more markup;

another attempt at more aggressive auto-loading (amending af28fdd50690) -- hidden buffers are now suppressed;

more frugal edits;

more explicit treatment of cleared nodes (removal is implicit);

clarified display;

more workarounds for scalac;

clarified display;

avoid redundant data structure;

more explicit discrimination of empty nodes -- suppress from Theories panel;

tuned;

tuned comments;

clarified module name: facilitate alternative GUI frameworks;

proper change of perspective for removed nodes (stemming from closed buffers);