make "ATP_Manager.get_prover" a total function, since we always want to show the same error text

remove some bloat

now rename the file "atp_wrapper.ML" to "atp_systems.ML" + fix typo in "SystemOnTPTP" script

renamed module "ATP_Wrapper" to "ATP_Systems"

move the minimizer to the Sledgehammer directory

remove debugging code

move some sledgehammer stuff out of "atp_manager.ML"

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