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

merged

reversed Tools to Actions Mirabelle renaming;

tuned;

reintroduce file offsets in Mirabelle output, but make sure they are not influenced by the length of the path

doc update

prefer evince over old xpdf -- NB: x86-cygwin bundles its own application;

cold-start HOME is user.home, in accordance with Cygwin-Terminal.bat;

chmod -x;

augment Isabelle home directory more systematically;

Cygwin setup via the quasi-mirror isabelle.in.tum.de, which serves a fixed (downgraded) version;

prevent change of directory, by pretending we are the "Command Here" utility;

typo

the perennial doc problem of how to define lists a second time

smoother handling of conjecture, so that its Skolem constants get displayed in countermodels

updated doc

add a timeout on the monotonicity check

handle TPTP definitions as definitions in Nitpick rather than as axioms

get rid of old parser, hopefully for good

fix handling of atomizable conjectures without a top-level "Trueprop" (e.g. "x == (y::nat)")

run Mirabelle in quick and dirty mode

doc update

scrollable text;

bundle Cygwin-Terminal.bat; tuned;

basic Cygwin-Terminal for main Isabelle directory;

moved to ~isatest/.bashrc to accomodate AFP;

merged

merged

doc update

NEWS

typedef with implicit set definition is considered legacy;

more standard method setup;

CONTRIBUTORS

added useful Trueprop_conv

move MRSL to a separate file

avoid conflict of Isabelle vs. Isabelle.exe on Cygwin;

more notes on Cygwin, notably for downgrading to 1.7.9 to avoid multi-threading instabilities starting with 1.7.10 early 2012;

CONTRIBUTORS

reworked Probability theory

updated test;

improved non-interpretation of constants and numbers; improved interpretation of terms and formulas; tuned;

improved interpreting conditionals; tuned;

disabled interpreting arithmetic;

improved handling of single-quoted names;

disabled exception packaging in tptp;

moved function for testing problem-name parsing; list of TPTP test files not immediately evaluated;

removed redundant function;

bundle Isabelle.exe;

tuned precedence order of transfer rules

updated generated files;

updated const "relcomp";

merged

add transfer rule for set difference

support Cygwin cold-start via Isabelle.exe, assuming layout of bundle;

merged

merged

adapt to changes in generated transfer rules (cf. 4483c004499a)

fix bug caused by misunderstanding of operator precedences (cf. cb44d09d9d22)

more robust handling of PATH vs PATH_JVM -- required for cold start of Cygwin from Windows (e.g. Isabelle.exe);

merged

fixed typos

tried harder to make SML/NJ happy