tweaked remote Vampire setup

update docs

killed SPASS 3.5/3.7 FLOTTER hack -- requires users to upgrade to SPASS 3.8

don't generate definitions for LEO-II -- this cuases more harm than good

dropped sort constraints on datatype specifications

potentially more convincing kill -TERM of feeder (cf. 32c03d45fffe) -- attempt to workaround spurious perl "hangs" on lxbroy10;

tuned proofs;

further attempts to simplify/robustify Swing_Thread.now, to avoid spurious physical race conditions on Java 6 / Mac OS X;

ignore empty messages even on tty, e.g. relevant for Isabelle_System.bash_output err output;

discontinued obsolete Cygwin module;

eliminated unused Cygwin download;

simplified Cygwin root: warm start via env, cold start via property, no registry magic;

include scala-compiler.jar in basic Isabelle/Scala environment, to make Isabelle/jEdit console work with scala-2.10.0-M3;

tuned proofs;

less warning in scala-2.10.0-M3;

avoid scala.tools.nsc.Interpreter -- deprecated in scala-2.9.0; discontinued support for scala-2.8.x;

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)

fixed soundness bug in Nitpick related to unfolding -- the unfolding criterion must at least as strict when looking at a definitional axiom as elsewhere, otherwise we end up unfolding a constant's definition in its own definition, yielding a trivial equality

more robust Swing_Thread.now: allow body to fail;

tuned proofs;

reparse descendants after update of imports, e.g. required for 'primrec' (line 17 of "src/HOL/Power.thy");

merged

update Satallax setup based on evaluation

merged

drop the feature that more than one quotient type can be defined by quotient_type -> it causes problems

prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule

gracefully handle definition-looking premises

simplified Poly/ML setup -- 5.3.0 is now the common base-line;

discontinued support for Poly/ML 5.2.1;

less specific sample usage;

some post-release notes;

tuned names

order LEO-II/Satallax definitions so that they build on each other (cf. Satallax's THF policy)

improved LEO-II definition handling -- still hoping for a fix directly in LEO-II

augment Satallax unsat cores with all definitions

better handling of incomplete TSTP proofs

generate THF definitions

build hybrid Isabelle component for JDK on x86-linux/x86_64-linux;

merged

eliminated old 'axioms';

discontinued obsolete method fastsimp / tactic fast_simp_tac;

eliminated obsolete fastsimp;

extend the Z3 proof parser to accept polyadic addition (on integers and reals) due to changes introduced in Z3 4.0

merged

doc updates

lower the monomorphization thresholds for less scalable provers

more explicit proof; misc tuning;

tuned proof;

prefer symbolic "contrib" -- mira should have a symlink to physical contrib_devel;

merged, abandoning change of src/HOL/Tools/ATP/atp_problem_generate.ML from 6ea205a4d7fd;

compile

don't apply "ext_cong_neq" to biimplications

added one slice with configurable simplification turned off

make higher-order goals more first-order via extensionality

added "ext_cong_neq" lemma (not used yet); tuning

use quot_del instead of ML code in Rat.thy