\DOC new_type

\TYPE {new_type : string * int -> unit}

\SYNOPSIS
Declares a new type or type constructor.

\DESCRIBE
A call {new_type(t,n)} declares a new {n}-ary type constructor called
{t} in the current theory segment. If {n} is zero, this is just a
new base type.

\FAILURE
Never fails, but issues a warning if the name is not a valid type
name. It will overwrite an existing type operator with the same name in
the current theory.

\EXAMPLE
A non-definitional version of ZF set theory might declare a new type {set} and
start using it as follows:
{
   - new_theory "ZF";
   <<HOL message: Created theory "ZF">>
   > val it = () : unit

   - new_type ("set", 0);
   > val it = () : unit

   - new_constant ("mem", Type`:set->set->bool`);
   > val it = () : unit

   - new_axiom ("EXT", Term`(!z. mem z x = mem z y) ==> (x = y)`);
   > val it = |- (!z. mem z x = mem z y) ==> (x = y) : thm
}


\SEEALSO
Theory.types, Theory.new_constant, Theory.new_axiom.
\ENDDOC
