renamed "Sledgehammer_Fact_Preprocessor" to "Clausifier"; the new name reflects that it's not used only by Sledgehammer (but also by "meson" and "metis") and that it doesn't only clausify facts (but also goals)

fewer dependencies

more intra-module dependency cleanup + merge "const" and "type_const" tables, since this is safe

more moving around of ML files in "Sledgehammer.thy"

got rid of needless exception

move "MESON" up; the ultimate goal is to make Sledgehammer depend on MESON and Metis, rather than a big spaghetti

remove junk

further reduce dependencies on "sledgehammer_fact_filter.ML"

move "prepare_clauses" from "sledgehammer_fact_filter.ML" to "sledgehammer_hol_clause.ML"; since it has nothing to do with filtering

merged

Quotient package reverse lifting

Add reverse lifting flag to automated theorem derivation

Restrict quotient definitions to constants

mixfix can be given for automatically lifted constants

streamlined the generation of quotient theorems out of raw theorems

merged

avoid REPEAT after THEN_ALL_NEW

refresh Isabelle token marker after buffer properties changed, e.g. when fold mode is switched;

treat alternative newline symbols as in Isabelle/ML;

simplified text_area_painter, with more precise treatment of visible line end;

merged

merged

eta-expand

improve the natural formula relevance filter code, so that it behaves more like the CNF one

split SPASS time slot between SOS and non-SOS, in case SOS times out

yields ill-typed ATP/metis proofs -- raus!

make sure "metisFT" is tried upon "metis" failure in "resolve_inc_tyvars"

merged

more direct definition simplifies proofs

merged

more precise tactic: do not escape to a different goal branch (REPEAT is still problematic, though)

a76ace919f1c wasn't quite right; second try

merge

never include anything from the Sledgehammer theory in the relevant facts + killed two obsolete facts

better eta-expansion in Sledgehammer's clausification; make the eta-expansion code more robust in the face of polymorphic arguments + make eta-expansion happen more often, since it first-orderizes things

cosmetics

make sure that theorems passed using "add:" to Sledgehammer are not eliminated on heuristic grounds

improve the new "natural formula" fact filter

explicit treatment of UTF8 sequences as Isabelle symbols;

ML pretty printing of type string according to (quasi-abstract) YXML markup and symbols (including UTF8);

escape UTF8 symbols for the ML compiler;

explicit treatment of UTF8 character sequences as Isabelle symbols;

slight cleaning and simplification of the automatic wrapper for quotient definitions

merged

export of proper information in the ML-interface of the quotient package

treat Pretty.T as strictly abstract type;

slightly more standard data merge: Symtax.merge (K true) avoids equality on abstract type Pretty.T and gracefully accepts overriding, Symtab.join prefers first entry as usual;

avoid equality on abstract type Pretty.T;

notes on packaging;

misc tuning;

tuned auxiliary structures;

Net.encode_type;

more accurate dependencies;

made smlnj happy

fix syntax bug in the TPTP output, by ensuring that "hBOOL" is correctly used for n-ary predicates even if (n + k)-ary occurrences of the same predicate, but with a different type, occur in the same problem

renamed for easier grep

use Skolem inlining also in the nonpolymorphic case, as a step toward simplifying the source code

steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs

have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry

fix bug with "skolem_id" + sort facts for increased readability

if SPASS fails at finding a proof with the SOS option turned on, turn it off and try again

merged

this looks like the most appropriate place to do the beta-eta-contraction

killed legacy "neg_clausify" and "clausify"

merged

factor out TPTP format output into file of its own, to facilitate further changes

merged

turn on "natural form" filtering in the Mirabelle tests, to see how it performs

missing "Unsynchronized" + make exception take a unit

added code to optionally perform fact filtering on the original (non-CNF) formulas

more cosmetics

cosmetics + prevent consideration of inlined Skolem terms in relevance filter

canonical argument order

leverage new data structure for handling "add:" and "del:"

thread original theorem along with CNF theorem, as a step toward killing the Skolem cache

merge "generic_prover" and "generic_tptp_prover"

removed Sledgehammer's support for the DFG syntax; this removes 350 buggy lines from Sledgehammer. SPASS 3.5 and above support the TPTP syntax.

distinguish between "unknown" and "no Kodkodi installed" errors

reintroduce new Sledgehammer polymorphic handling code; this time I tested the proper version of Isabelle

make the Nitpick_Example theory processable even when Kodkodi is not installed; so that at least the "theory" aspects of it (as opposed to the diagnosis offered by Nitpick) are checked on everybody's machines

Make latex happy

Quotient package now uses Partial Equivalence instead place of equivalence

Replace 'list_rel' by 'list_all2'; they are equivalent.

Proper treatment of non-inherited mixins.

merged

Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.

reredisable new polymorphic code

merged

beta-eta was too much, because it transformed SOME x. P x into Eps P, which caused problems later; reintroduced old proof based on Metis, since it was a good test for the Skolemizer

back to post-release mode;

merged, resolving conflicts in doc-src/IsarRef/Thy/HOL_Specific.thy;

make Nitpick's unsound mode a bit more unsound

sort cases on the proper key

compile

thread "full_types"

try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better

clean up after fcc768dc9dd0

adjusted Nitpick examples to latest changes + make them slightly faster

optimized code generated for datatype cases + more; more = lazy creation of debugging messages in mono code + use of "let" when performing some beta-applications (to avoid exponential blowup) + removal of some set constructs, to simplify the code and increase precision in some cases (and decrease it in others, but this can be regained)

activated Scala code generator test

added bot instances; tuned

extensionality rule fset_eqI

merged

separate section for diagnostic commands

more binding; avoid arcane Rep and Abs prefixes

cleanup of typecopy package

quickcheck for fsets

merged

added pigeonhole lemmas

merged

tuned whitespace; dropped dead code

code_simp: only succeed on real progress

prefer fold over foldl

conclude simplification with default simpset

drop subsumed default equations (requires a little bit unfortunate laziness)

avoid Scala legacy operations

prefer fold over foldl

made List.thy a join point in the theory graph

tuned set_replicate lemmas

merged

added lemmas

dropped dead code

replaced unreliable metis proof

rev is reverse in Haskell

first serious draft of a scala code generator

more precise code

explicit type variable arguments for constructors

transitive superclasses were also only a misunderstanding

formal introduction of transitive superclasses

dropped obscure type argument weakening mapping -- was only a misunderstanding

added simp evaluator

merged

added code_simp infrastructure

tuned whitespace

maintain cong rules for case combinators; more precise permissiveness

drop function definitions of combinators

maintain cong rules for case combinators

formal introduction of case cong

found missing beta-eta-contraction

added missing Umlaut

make example run a bit faster (might help atbroy102)

merged

tuned documents

teaked naming of superclass projections

added lemma funpow_mult

extended bib

updated generated code

added reference

subsection on locale interpretation

explicitly name and note equations for class eq

use various predefined Haskell operations when generating code

NEWS

tuned internal order

dropped unused bindings

corrected syntax diagram

turn off new polymorphism code again -- a new issue popped up

missing case

A function called "untyped_aconv" shouldn't look at the bound names!

no point in introducing combinators for inlined Skolem functions

better error reporting for Vampire

expect SPASS 3.7, and give a friendly warning if an older version is used

improve ATP-specific error messages

merged

removed simplifier congruence rule of "prod_case"

adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"

merged

declare lexn.simps [code del]

declare lex_prod_def [code del]

modernized specifications

avoid references to old constdefs

merged

disable new polymorphic code for now, until remaining issues in "equality_inf" are resolved

"raise Fail" for internal errors + one new internal error (instead of "Match")

make test work again (broken since 09467cdfa198?)

adjust Nitpick example to follow latest wave of renamings

proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter

beta-eta-contract, to respect "first_order_match"'s specification; Sledgehammer's Skolem cache sometimes failed without the contraction

adjust Nitpick's handling of "<" on "rat"s and "reals"

remove needless variables

hide sum explicitly

merged

adjust popular symbolic type constructors

tailored set of code equations manually

tuned quotes, antiquotations and whitespace

moved inductive_codegen to place where product type is available; tuned structure name

qualified type "*"; qualified constants Pair, fst, snd, split

tuned quotes, antiquotations and whitespace

qualified types "+" and nat; qualified constants Ball, Bex, Suc, curry; modernized some specifications

Adapted Mirabelle script (cf. f60e4dd6d76f)

merged

more consistent naming aroud type classes and instances

back to non-release mode;