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;

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;

proper checking of ML functors (in Poly/ML 5.2 or later); eliminated pathetic comments;

added ML antiquotation @{make_string}, which produces proper pretty printed version in Poly/ML 5.3.0 or later;

isatest: improved treatment of local files on atbroy102;

add rule deflation_ID to proof script for take + constructor rules

more robust record syntax: use Type.raw_match to ignore sort constraints as in regular abbreviations (also note that constraints only affect operations, not types);

HOL record: explicitly allow sort constraints;

misc tuning and simplification;

explicit ProofContext.check_tfree;

merged

Respectfullness and preservation of list_rel

replaced slightly odd Typedecl.predeclare_constraints by plain declaration of type arguments -- also avoid "recursive" declaration of type constructor, which can cause problems with sequential definitions B.foo = A.foo; simplified via ProofContext.check_tfree;

get_sort: suppress dummyS from input; added check_tvar, check_tfree convenience; tuned;

modernized treatment of sort constraints in specification; pass-through type variables as usual as (string * sort) internally -- recovers proper sort handling;

typecopy: observe given sort constraints more precisely;

inline old Record.read_typ/cert_typ; spelling;

spelling;

theory RBT with abstract type of red-black trees backed by implementation RBT_Impl

tuned whitespace;

merged

merged

added "overlord" option (to get easy access to output files for debugging) + systematically use "raw_goal" rather than an inconsistent mixture

make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second

make Sledgehammer's "timeout" option work for "minimize"

fixed handling of "sledgehammer_params" that get a default value from Isabelle menu; and added "atp" as alias for "atps"

Spelling error: theroems -> theorems

advertise [rename_abs] attribute in LaTeXsugar -- wish I had known about this earier.