----------------------------------------------------------------------
new_binder                                                (boolSyntax)
----------------------------------------------------------------------
new_binder : string * hol_type -> unit

SYNOPSIS
Sets up a new binder in the current theory.

DESCRIBE
A call {new_binder(bnd,ty)} declares a new binder {bnd} in the
current theory. The type must be of the form {('a -> 'b) -> 'c}, because
being a binder, {bnd} will apply to an abstraction; for example

   !x:bool. (x=T) \/ (x=F)

is actually a prettyprinting of

   $! (\x. (x=T) \/ (x=F))




FAILURE
Fails if the type does not correspond to the above pattern.

EXAMPLE

   - new_theory "anorak";
   > val it = () : unit

   - new_binder ("!!", (bool-->bool)-->bool);
   > val it = () : unit

   - Term `!!x. T`;
   > val it = `!! x. T` : term




SEEALSO
Theory.constants, Theory.new_constant, boolSyntax.new_infix,
Definition.new_definition, boolSyntax.new_infixl_definition,
boolSyntax.new_infixr_definition, boolSyntax.new_binder_definition.

----------------------------------------------------------------------