new_binder : string * hol_type -> unit
STRUCTURE
boolSyntax
SYNOPSIS
Sets up a new binder in the current theory.
DESCRIPTION
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
constants, new_constant, new_infix, new_definition, new_infixl_definition, new_infixr_definition, new_binder_definition
HOL  Trindemossen-1