repaired snag in debug function

graceful handling of Waldmeister endgame

improve parsing of Waldmeister dependencies (and kill obsolete hack)

tuning

added debugging function

LEO-II's "--sos" option confusingly disables rather than enables SOS, and SOS seems to be ignored anyway; also, pass a number of facts that's more appropriate for each prover

eta-reduce definition-like equations for THF provers; Satallax in particular seems to love that

get rid of "conj_sym_kind" -- most interesting provers now have built-in sorts, and for the others (e.g. E) "Hypothesis" isn't too bad a default

extend ATP data structure to avoid having to perform ((non-)capture avoiding) beta reduction -- fixes a bug in the THF translation of "is_measure.simps"

reintroduced example now that it's no longer broken

fixed "real" after they were redefined as a 'quotient_type'

temporarily comment out broken nitpick example; adapt to new definition of type rat

simplify instance proofs for rat

convert Rat.thy to use lift_definition/transfer

cleaner handling of bi-implication for THF output of first-order type encodings

distinguish between instantiated and uninstantiated inductions -- the latter are OK for first-order provers

temporarily comment out broken nitpick example

convert real number theory to use lifting/transfer

tuned ordering of lemmas

pass fewer facts to LEO-II and Satallax

tweak LEO-II setup

use raw monomorphic encoding with Waldmeister, to avoid overloading it with too many function symbols (as would be the case using mangled monomorphic encodings)

build Pure_64 with new settings

tuned

playing around with mira settings

defining and proving Executable_Relation with lift_definition and transfer

specialised fact in the Record theory should not be appear in proofs discovered by sledgehammer

prevent spurious timeouts

added "try0" tool to Mirabelle

use latest E (1.5)

lifting package produces abs_eq_iff rules for total quotients

using the new transfer method to obtain abstract properties of RBT trees

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

removed obsolete RC tags;

Added tag Isabelle2012 for changeset 21c42b095c84

try to avoid races again (cf. 8c37cb84065f and fd3a36e48b09);

Added tag Isabelle2012-RC3 for changeset ed5f56b8f90a

some message;

tuned error -- reduce potential for confusion in a higher-level context, e.g. partial checking of theory sub-graph;

Fixed disambiguation of names (cf. 5759ecd5c905)

merged

file.encoding=UTF-8 for java.ext.dirs, to agree with java runtime invocation;

prefer absolute paths, to allow launching from a different context (e.g. via file associations);

tweaked Inductive.prove_eqs to allow degenerate definition like "inductive TRUE where TRUE";

allow spaces in target directory;

Added tag Isabelle2012-RC2 for changeset 1636ff4c6243

init Cygwin after unpacking;

tuned proofs;

more accurate ROOT.ML;

prefer http://isabelle.in.tum.de/library alias, which is available at TUM only;

some highlights of Isabelle2012;

refrain from SIGHUP handling (cf. 5f629ee2502b), which does not work on Cygwin and appears to be redundant anyway (no extra output produced within pipe);

some attempts to make critical errors fit on screen;

more NEWS;

backout 9579464d00f9 to avoid odd crash of polyml-5.2.1 (according to Jasmin, this change is not essential for now);

Added tag Isabelle2012-RC1 for changeset ec5d54029664