adding more profiling to the predicate compiler

only add relevant predicates to the list of extra modes

switched off no_topmost_reordering

replaced call to inductive package by axiomatization in the function flattening of the predicate compiler

added option for specialisation to the predicate compiler

prefer functional modes of functions in the mode analysis

added peephole optimisations to the predicate compiler; added structure Predicate_Compile_Simps for peephole optimisations

merged

Only use provided SMT-certificates in HOL-Multivariate_Analysis.

Translated remaining theorems about integration from HOL light.

marked cygwin-poly as "e" test, which means further stages do not depend on it (website etc.);

replace many uses of Drule.export_without_context with Drule.zero_var_indexes

Remove garbage.

Remove garbage.

recovered isabelle java, which was broken in ebfa4bb0d50f;

fix bug in SPASS's DFG output files, where "tc_bool" wasn't declared; this bug occurs when the explicit "hAPP" or "hBOOL" functions are introduced and full types is activated

merged

added "explicit_apply" option to Sledgehammer, to control whether an explicit apply function should be used as much or as little as possible (replaces a previous global variable)

merge

cosmetics

don't redo an axiom selection in the first round of Sledgehammer "minimize"!; this is needlessly slow and messes up the declared functions/predicates in SPASS DFG files

get rid of "conjecture_pos", which is no longer necessary now that it's Metis's job, not Sledgehammer's, to report inconsistent contexts

added warning about inconsistent context to Metis; it makes more sense here than in Sledgehammer, because Sledgehammer is unsound and there's no point in having people panicking about the consistency of their context when their context is in fact consistent

workaround for Proof General's off-by-a-few sendback display bug, whereby "pr" in "proof" is not highlighted

got rid of somewhat pointless "pairname" function in Sledgehammer

make Sledgehammer's "add:" and "del:" syntax really work (I hope), by comparing CNF theorems with CNF theorems

cosmetics

cosmetics

cosmetics

make Sledgehammer's minimizer also minimize Isar proofs

don't use readable names if proof reconstruction is needed, because it uses the structure of names

allow "_" in TPTP names in debug mode

rename Sledgehammer "theory_const" option to "theory_relevant", now that I understand better what it does

set SPASS option on the command-line, so that it doesn't vanish when moving to TPTP format

get rid of "List.foldl" + add timestamp to SPASS

less ambitious settings for cygwin-poly;

respectfullness and preservation of map for identity quotients

respectfullness and preservation of function composition

eta-normalize the goal since the original theorem is atomized

accept x86_64 results gracefully -- NB: Mac OS does report that if booted in 64 bit mode;

refer to THIS_JAVA dynamically, and treat ISABELLE_JAVA as static default -- relevant for nested JVM invocation within an existing Isabelle enviroment;

merged

more appropriate representation of valid positions for abstractors

more appropriate representation of valid positions for abstractors; more accurate checking of abstype certificates

update_syntax: add new productions only once, to allow repeated local notation, for example;

tuned;

more platform information;

check JVM platform at most once -- still non-strict to prevent potential failure during initialization of object Platform;

some updates on multi-platform support;

merged

explicit check sorts in abstract certificates; abstractor is part of dependencies

polyml-platform script is superseded by ISABELLE_PLATFORM;

less ambitious settings for cygwin-poly;

merged

more convenient equations for zip

more platform info;

added ISABELLE_PLATFORM and ISABELLE_PLATFORM64 -- NB: ML and JVM may have a different idea;

system properties determine the JVM platform, not the Isabelle one;

THIS_CYGWIN;

improved ISABELLE_JAVA, based on THIS_JAVA of the actually running JVM;