Calc
Inductive()
Lemma
NewType()
Proof
QExists()
QForAll()
Struct()
axiom()
cond()
define()
prove()
search()
simp()
BaseSolver
EProverTHFSolver
LeoIIISolver
MultiSolver
NanoCopISolver
SATSolver
TweeSolver
VampireSolver
VampireTHFSolver
ZipperpositionSolver
binpath()
collect_decls()
collect_sorts()
expr_to_smtlib()
expr_to_tptp()
funcdecl_smtlib()
install_solvers()
mangle_decl()
mangle_decl_smtlib()
run()
smt2tptp()
smtlib_datatypes()
sort_to_tptp()
tptp2smt()
get_vars()
interp()
interp_pred()
interp_term()
prolog()
run_string()
e (ExprRef)
list[ExprRef]