Calc
FreshVar()
FreshVars()
Inductive()
Lemma()
NewType()
PTheorem()
Proof
QExists()
QForAll()
QImplies()
Struct()
Theorem()
axiom()
cond()
define()
prove()
search()
simp()
register_definition()
Judgement
LemmaError
Unfolding
andI()
choose()
compose()
decl_occurs()
declare()
define_fix()
define_simple()
defns
ext()
forget()
free_vars()
fresh_const()
generalize()
herb()
induct_inductive()
instan()
is_declared()
is_defined()
is_fresh_var()
is_proof()
make_unfolding()
modus()
obtain()
open_binder()
rename_vars2()
specialize()
subst()
trigger()
unfold()
unfold_defns()
Can register other unfoldings besides those generated by define. This may be useful to get unfolding for objects constructed in roundabout ays.
defn (Unfolding)