some updates on classic README, reduce the impression that there is much to install manually;

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

get rid of old CASC setup and move the arithmetic part to a new theory

smaller batches, to play safe

move file to where it belongs

implement transfer tactic with more scalable forward proof methods

tuning

tweak LEO-II setup

eta-expand unapplied equalities in THF rather than using a proxy

more tweaking of TPTP/CASC setup

added a basic sanity check for quot_map

tuned comment;

fixed bug in handling of new numerals -- the left-hand side of "Numeral1 = 1" should be left alone and not translated to a built-in Kodkod numeral in the specification of the "numeral" function

merged

add code equation for real_of_float

tuned; don't generate abs code if quotient_type is used

support Quotient map theorems with invariant parameters

use a quot_map theorem attribute instead of the complicated map attribute

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

put Satallax first, at least for now (useful for experiments)

tuning

tuning

tentatively tag hypotheses as definition -- this sometimes help the "tptp_sledgehammer" tool (e.g. SEU466^1.p)

tuning; no need for relevance filter

tuning

don't extensionalize formulas for higher-order provers -- Satallax in particular will only expand definitions of the form "constant = ..."

don't use the native choice operator if the type encoding isn't higher-order

tuning

more work on TPTP Isabelle and Sledgehammer tactics

more work on CASC setup

more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;

mingw is windows (still inactive);

add Caratheodories theorem for semi-rings of sets

moved lemmas to appropriate places

register polyml executables so that Cygwin rebaseall will see them;

merged

smarter PDF_VIEWER defaults, based on hints by Lars Noschinski;

equate positive Lebesgue integral and MV-Analysis' Gauge integral

correct lemma name

tweak TPTP Nitpick's output

remove too aggressive skolemization optimization (prevented discovery of a model in SYN994^1)

improve precision (noticed on SEV296^5.thy) -- the exception for "bool" used to be necessary because of a hack where "opt" meant two different things

output SZS status as early as possible

sorted lemma list in NEWS

merged

reactivated ListCellRenderer for Java 6 (cf. b9e2ed4b1579, 0ddac15782e4, de249b5ae6e2);

enforce our JAVA_HOME to avoid potential conflicts with other Java installations by the user;

updated README;

include generated application wrapper;

back to mature jdk1.6.0_31, to avoid issues like Sidekick TAB completion and generic ListCellRenderer;

ISABELLE_JDK_HOME is already provided by isatest shell environment;

added splash screen, to reduce confusion when waiting for main application to start up;

move polyml within Cygwin /usr/local to simplify its rebasing;

improved spelling;

added "no_atp"s for extremely prolific, useless facts for ATPs

tuned;

merged

made "split_last" more robust in the face of obscure low-level errors

removed confusing error

some friendly message;

merged

merged

merged