rhs of abstract code equations are not subject to preprocessing: inline code abbrevs explicitly

renamed Semi to Seq

merged

prefer Context_Position.report_generic, which observes is_visible flag and thus reduces number of echos;

clarified signature;

avoid spurious warning in invisible context, notably Haftmann-Wenzel sandwich;

made Context_Position independent from Config;

use Nitpick as an oracle for finite problems

add extensionality to first-order provers

avoid duplicate helpers

mention tools and packages earlier;

tuned;

tuned;

tuned;

tuned;

merged

allow transfer tactic to leave extra unsolved subgoals if transfer rules are missing

documentation for the Lifting package in Isar-ref

added darwin targets;

chmod -x;

multi-platform build script and component settings;

print errors on stderr;

general exec_process -- nothing specific to Cygwin;

more direct exec with synchronous exit code;

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;