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;

isatest: more robust treatment of remote files, less reliance on mounted file system;

merged

added missing \n in output

by default, don't try to start ATPs that aren't installed

fiddle with Sledgehammer option syntax

added timestamp to proof

restore order of clauses in TPTP output; there's a rather subtle invariant w.r.t. "extract_lemmas"

optimize relevance filter by doing a Table.fold directly rather than destroying the datastructure each time; saves 2 sec per Sledgehammer invocation on my laptop!

output total time taken by Sledgehammer if "verbose" is set

Sledgehammer: the empty set of fact () should mean nothing, not unchanged

reorganize Sledgehammer's relevance filter slightly

tell the user that Sledgehammer kills its siblings

updated keywords;

replaced old Sign.add_tyabbrs(_i) by Sign.add_type_abbrev (without mixfix); misc tuning and simplification;

keep localized 'types' as regular non-old-style version -- 'type_abbrev' as 'type' just causes too many problems, e.g. clash with "type" in translations or "type:" argument syntax;

separate commands 'hide_class', 'hide_type', 'hide_const', 'hide_fact';

replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;

allow syntax types within abbreviations;

modernized old-style type abbreviations;

modernized type abbreviations;

local type abbreviations;

merged

added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)

store nonmangled names along with mangled type names in Sledgehammer for debugging purposes

give more sensible names to "fol_type" constructors, as requested by a FIXME comment

make Sledgehammer's output more debugging friendly

made SML/NJ happy;

proper masking of dummy name_space;

salvaged some ML functors from decay, which is the natural consequence of lack of formal checking;