Calc
FreshVar()
FreshVars()
Inductive()
Lemma()
NewType()
PTheorem()
Proof
QExists()
QForAll()
QImplies()
Struct()
Theorem()
axiom()
cond()
define()
prove()
search()
simp()
simp1()
Order
RewriteRule
RewriteRuleException
Rule
all_narrow()
apply()
backward_rule()
beta()
decl_index()
def_eq()
esimp()
forward_rule()
full_simp()
horn_trig()
kbo()
lpo()
rewrite()
rewrite1()
rewrite1_rule()
rewrite_of_expr()
rewrite_once()
rewrite_slow()
rule_of_expr()
rw_trig()
simp2()
unfold()
simplify a term using z3 built in simplifier
t (ExprRef)
ExprRef