give an error if no ATP is set

move the Sledgehammer menu options to "sledgehammer_isar.ML"

centralized ATP-specific error handling in "atp_wrapper.ML"

handle ATP proof delimiters in a cleaner, more extensible fashion

merged

fix another if-then-else parse error

fix if-then-else parse error

merged

fix syntax precedence declarations for UNION, INTER, SUP, INF

syntax precedence for If and Let

fix lots of looping simp calls and other warnings

fix duplicate simp rule warnings

define finer-than ordering on net type; move some theorems into Limits.thy

generalize type of continuous_on

define nets directly as filters, instead of as filter bases

use 'example_proof' (invisible);

command 'example_proof' opens an empty proof body;

proofs that are discontinued via 'oops' are treated as relevant --- for improved robustness of the final join of all proofs, which is hooked to results that are missing here;

eliminanated some unreferenced identifiers; tuned;

merged

add bounded_lattice_bot and bounded_lattice_top type classes

merged

dropped group_simps, ring_simps, field_eq_simps

class division_ring_inverse_zero

dropped group_simps, ring_simps, field_eq_simps; classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero

line break

removed unused AxClass.class_intros;

updated Sign.add_type_abbrev;

merged

field_simps as named theorems

merged

generalize more constants and lemmas

simplify types of path operations (use real instead of real^1)

add lemmas convex_real_interval and convex_box

generalize more constants and lemmas

generalize constant closest_point

minimize imports

fix imports

document generation for Multivariate_Analysis

move l2-norm stuff into separate theory file

convert proofs to Isar-style

Library/Fraction_Field.thy: ordering relations for fractions

renamed Drule.unconstrainTs to Thm.unconstrain_allTs to accomdate the version by krauss/schropp; less pervasive names;

more systematic treatment of data -- avoid slightly odd nested tuples here; tuned;

replaced Sorts.rep_algebra by slightly more abstract selectors classes_of/arities_of;

misc tuning and simplification;

simplified some private bindings;

classrel and arity completion by krauss/schropp;

removed obsolete/unused Proof.match_bind;

modernized naming conventions of main Isar proof elements;

goals: simplified handling of implicit variables -- removed obsolete warning;

updated generated files;

cover 'schematic_lemma' etc.;

mark schematic statements explicitly;

eliminated spurious schematic statements;

explicit 'schematic_theorem' etc. for schematic theorem statements;

collapse category "schematic goal" in keyword table -- Proof General does not know about this;

added keyword category "schematic goal", which prevents any attempt to fork the proof;

merged

merged

separated instantiation of division_by_zero

epheremal replacement of field_simps by field_eq_simps; dropped old division_by_zero instance

adapted to new times_divide_eq simp situation

epheremal replacement of field_simps by field_eq_simps

dequalified fact name

sharpened constraint (c.f. 4e7f5b22dd7d); explicit is better than implicit

separated instantiation of division_by_zero

dequalified fact name

less special treatment of times_divide_eq [simp]

sharpened constraint (c.f. 4e7f5b22dd7d)

more localization; tuned proofs

more localization; factored out lemmas for division_ring

modernized abstract algebra theories

merged

swapped generic code generator and SML code generator

removed obsolete Named_Thm_Set -- Named_Thms provides efficient member operation;

Item_Net/Named_Thms: export efficient member operation;

initialized atps reference with standard setup in the atp manager

compile

handle SPASS's equality predicate correctly in Isar proof reconstruction

merged

added Isar proof reconstruction support for SPASS -- which means all provers can now yield Isar proofs; the implementation might still be flaky, but exceptions are caught so that a proof reconstruction failure doesn't result in a Sledgehammer failure (the one-line Metis proof might still work after all)

remove hack that is no longer necessary now that "ATP_Wrapper" properly detects which ATPs are installed

set "atps" reference's default value to "(remote_)e (remote_)spass (remote_)vampire", based on what is installed

minor code cleanup

if Isar proof reconstruction is not supported, tell the user so they don't wonder why their "isar_proof" option did nothing

"remote_e" and "remote_vampire" support TSTP proof output + fix "overlord" mode ATP output postprocessing

Isar proof reconstruction: type variables introduced by the ATP should be treated as type parameters for type inference purposes; this solves the unification exception that consistently was thrown for Cezary's "FSet3" theory

postprocess ATP output in "overlord" mode to make it more readable

failure of reconstructing the Isar proof (e.g., exception) should not prevent Sledgehammer from showing the short one-liner proof -- but in "debug" mode we do want to know what the exception is

generate command-line in addition to timestamp in ATP output file, for debugging purposes

pass relevant options from "sledgehammer" to "sledgehammer minimize"; one nice side effect of this change is that the "sledgehammer minimize" syntax now only occurs in "sledgehammer_isar.ML", instead of being spread across two files

Finite set theory

merged

Tidied up using s/l

split Class.thy into parts to conserve a bit of memory and increase the chance of making it work on Cygwin with only 2 GB available;

fun_rel introduction and list_rel elimination for quotient package

lemmas concerning remdups

lemma dlist_ext

merged

optionally ignore errors during translation of equations; tuned representation of abstraction points

optionally ignore errors during translation of equations

tolerate eta-variants in f_graph.cases (from inductive package); added test case;

simplified example

use only one thread in "Manual_Nits"; the second thread isn't helping much, and might very well be the cause of the Cygwin Isatest failure

merged

clarify error message

distinguish between the different ATP errors in the user interface; in particular, tell users to upgrade their SPASS if they try to run "spass_tptp" with an old SPASS version with no TPTP support

added "spass_tptp" prover, which requires SPASS x.y > 3.0; once users have upgraded their SPASS and we have determined that "spass_tptp" works well, we can make "spass_tptp" the one and only "spass"

use "Proof.goal" in Sledgehammer's minimizer (just like everywhere else in Sledgehammer), not "Proof.raw_goal"

merged

make profiling depend on reference Quickcheck.timing

added examples for detecting switches

adopting documentation of the predicate compiler

removing dead code; clarifying function names; removing clone

adopting examples to changes in the predicate compiler

adopting quickcheck

tuning mutabelle; adding output of mutant theoryfile for interactive evaluation

added switch detection to the predicate compiler

added further inlining of boolean constants to the predicate compiler

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;

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.

record package: corrected sort handling in type translations to avoid crashes when default sort is changed. Test case: record 'a T = elem :: 'a defaultsort order term elem (* low-level exception *)

more precise treatment of UNC server prefix, e.g. //foo;

support named_root, which approximates UNC server prefix (for Cygwin); tuned representation: reversed elements; misc simplification and cleanup;

updated Thm.add_axiom/add_def;

adapted PUBLISH_TEST for atbroy102, which only mounts /home/isatest;