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