new_binder_definition : string * term -> thm
Let v1, ..., vn be syntactically distinct tuples constructed from the variables x1,...,xm. A binder is defined by evaluating
new_binder_definition (name, `b v1 ... vn = t`)
|- !x1...xn. b v1 ... vn = t
The equation supplied to new_binder_definition may optionally have any of its free variables universally quantified at the outermost level. The constant b has binder status only after the definition has been made.
- new_binder_definition (`EXISTS_UNIQUE_DEF`, Term`$?! = \P:(*->bool). ($? P) /\ (!x y. ((P x) /\ (P y)) ==> (x=y))`); > val it = |- $?! = (\P. $? P /\ (!x y. P x /\ P y ==> (x = y))) : thm
new_binder_definition(name, Term `$b = ... `);