really minimize sorts after certification -- looks like this is intended here;

tuned signature;

merged

tuned whitespace

got rid of [simplified]

got rid of [simplified]

fix SML/NJ compilation (I hope)

tuned classrel completion -- bypass composition with reflexive edges;

tuned diff_classrels -- avoid slightly inefficient Symreltab.keys;

tuned aritiy completion -- slightly less intermediate data structures;

clarified proven results: store thm only and retrieve proof later via Thm.proof_of (this may also impact parallelism, because internal join_proofs is deferred);

misc tuning and simplification;

NEWS and CONTRIBUTORS

explicit is better than implicit

tuned class linordered_field_inverse_zero

merged

instances for *_inverse_zero classes

canonical import

merged

use new classes (linordered_)field_inverse_zero

merged

renamed option

fixes 2a5c6e7b55cb; do not throw out the baby with the bath water

compile

make compile (and not just load dynamically)

merge

introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method; the code is still somewhat experimental but any exceptions it throws are catched, and Sledgehammer will still yield a one-line metis proof in case of proof reconstruction failure

adapt code to reflect new signature of "neg_clausify"

rename options and keep track of conjecture shape (to facilitate proof reconstruction)

rename options

make "neg_clausify" return a list of lists of clauses, so that it's possible to see which clause comes from which theorem

remove needless code that was copy-pasted from Quickcheck (where it made sense)

cosmetics

cosmetics

move "neg_clausify" method and "clausify" attribute to "sledgehammer_isar.ML"

support readable names even when Isar proof reconstruction is enabled -- useful for debugging

cosmetics: rename internal functions

cosmetics

remove "show_skolems" option and change style of record declarations

remove "skolemize" option from Nitpick, since Skolemization is always useful

removed Nitpick's "uncurry" option

fix typesetting

Fruhjahrsputz: remove three mostly useless Nitpick options

remove type annotations as comments; Nitpick is now 1136 lines shorter

cosmetics

better error reporting; in particular, users shouldn't panic if "metis" can prove "False", especially in "neg_clausify"-style proofs

cosmetics

reuse timestamp function

stop referring to Sledgehammer_Util stuff all over Nitpick code; instead, redeclare any needed function in Nitpick_Util as synonym for the Sledgehammer_Util function of the same name

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