merged

"prod" and "sum" replace "*" and "+" respectively; qualified constants Set.member and Set.Collect

"prod" and "sum" replace "*" and "+" respectively

qualified constants Set.member and Set.Collect

"prod" and "sum" replace "*" and "+" respectively; qualified constants Set.member and Set.Collect

merged

convert theorem path_connected_sphere to euclidean_space class

generalize more lemmas from ordered_euclidean_space to euclidean_space

avoid Old_Number_Theory; more precise dependencies;

misc tuning and modernization;

merged

once more a try with mkdir_leaf

refined semantics of mkdir_leaf: do not fail if directory already exists

avoid bitstrings in generated code

Updated NEWS

Add theory for indicator function.

Instantiate product type as euclidean space.

merged

repaired line ending

revert to plain for now mkdir

one unified Word theory

more speaking names

more speaking names

moved specific operations here

more speaking theory names

more speaking theory names

use existing bit type from theory Bit

split off Cardinality from Numeral_Type

added literal and typerep instances

mkdir_leaf -- avoiding surprises with typos in user-given paths

generalize some lemmas about derivatives

add lemma at_within_interior

generalize more euclidean_space lemmas

minimize dependencies on Numeral_Type

change type of 'dimension' to 'a itself => nat

generalize some euclidean_space lemmas

merged

rewrote the TPTP problem generation code more or less from scratch; there is now an explicit AST data structure which will make it easy to support alternative formats (e.g., DFG, sorted TPTP, sorted DFG); also, if "full_types" is enabled, "hAPP" is then tagged properly

rename functions

merged

unfold_fun_n

pervasive tuning of code

explicit printing function for applify

fail with low-level exception, not user error;

eliminated some unused bindings;

recovered some indentation from the depths of time;

cleaned by using descending instead of lifting

merged

move function

compile

compile

more elegant cheating

Sledgehammer can save some msecs by cheating

more precise error message for remote ATPs

move blacklisting completely out of the clausifier; the only reason it was in the clausifier as well was the Skolem cache

rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems

move "nice names" from Metis to TPTP format

move functions not needed by Metis out of "Metis_Clauses"

no setup is necessary anymore

adapt call

remove obsolete component of CNF clause tuple (and reorder it)

killed "expand_defs_tac"; it has no raison d'etre now that Skolemization is always done "inline"; the comment in the code suggested that it was used for other things as well but the code clearly did nothing if no Skolem "Frees" were in the problem

get rid of Skolem cache by performing CNF-conversion after fact selection

always perform "inline" skolemization, polymorphism or not, Skolem cache or not

always perform relevance filtering on original formulas

merged

split off predicate compiler into separate theory

split off predicate compiler into separate theory

adapted to reorganization of auxiliary list operations; split off predicate compiler into separate theory

adapted to change in interface

updated generated document

tuned

merged

tuned theory text

inner_simps is not enough, need also local facts

put section on distinctness before listsum; refined code generation operations; dropped ancient infix mem

explicit is better than implicit

avoid List.all

tuned whitespace

tuned lemma formulations

list_ex replaces list_exists

tuned syntax

explicit is better than implicit

modernized specifications

dropped ancient infix mem

dropped ancient infix mem; refined code generation operations in List.thy

cosmetics: avoided statement of raw theorems, used the method descending instead

separated the lifting and descending procedures in the quotient package

separation of translations in derive_qtrm / derive_rtrm (similarly for types)

merged constants "split" and "prod_case"

merged constants "split" and "prod_case" -- nitpick behaves differently

tuned whitespace

merged

compile

merged

multiplexing

factor out thread creation

factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration

update docs

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