zDefine : term quotation -> thm
STRUCTURE
bossLib
SYNOPSIS
General-purpose function definition facility.
DESCRIPTION
zDefine behaves exactly like Define, except that it does not add the definition to computeLib.the_compset. Consequently the definition is not used by bossLib.EVAL when evaluating expressions.

FAILURE
zDefine and Define succeed and fail in the same way.

EXAMPLE
- zDefine `foo = 10 ** 10 ** 10`
- EVAL ``foo``;
> val it = |- foo = foo: thm

COMMENTS
zDefine is helpful when users wish to derive and use their own efficient evaluation theorems, which can be added using computeLib.add_funs or computeLib.add_persistent_funs.
SEEALSO
Define
HOL  Kananaskis-14