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