simpler argument

got rid of "respect_no_atp" option, which even I don't use

reorder ML files

renamed "Sledgehammer_FOL_Clauses" to "Metis_Clauses", so that Metis doesn't depend on Sledgehammer

merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME

get rid of type alias

exploit "Name.desymbolize" to remove some dependencies

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;